Loogle!

Result

Found 184 declarations mentioning Ordinal.type.

• Ordinal.type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal.{u}
• Ordinal.type_empty 📋 Mathlib.SetTheory.Ordinal.Basic
  : Ordinal.type emptyRelation = 0
• Ordinal.type_pEmpty 📋 Mathlib.SetTheory.Ordinal.Basic
  : Ordinal.type emptyRelation = 0
• Ordinal.type_pUnit 📋 Mathlib.SetTheory.Ordinal.Basic
  : Ordinal.type emptyRelation = 1
• Ordinal.type_unit 📋 Mathlib.SetTheory.Ordinal.Basic
  : Ordinal.type emptyRelation = 1
• Ordinal.card_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (Ordinal.type r).card = Cardinal.mk α
• Ordinal.inductionOn 📋 Mathlib.SetTheory.Ordinal.Basic
  {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r], motive (Ordinal.type r)) : motive o
• Cardinal.ord_le_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [h : IsWellOrder α r] : (Cardinal.mk α).ord ≤ Ordinal.type r
• Ordinal.type_eq_zero_of_empty 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [IsEmpty α] : Ordinal.type r = 0
• Ordinal.type_ne_zero_of_nonempty 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [h : Nonempty α] : Ordinal.type r ≠ 0
• Ordinal.type_eq_zero_iff_isEmpty 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : Ordinal.type r = 0 ↔ IsEmpty α
• Ordinal.type_ne_zero_iff_nonempty 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : Ordinal.type r ≠ 0 ↔ Nonempty α
• Ordinal.type_eq_one_iff_unique 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : Ordinal.type r = 1 ↔ Nonempty (Unique α)
• Ordinal.type_eq_one_of_unique 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [Nonempty α] [Subsingleton α] : Ordinal.type r = 1
• Ordinal.type_fintype 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] [Fintype α] : Ordinal.type r = ↑(Fintype.card α)
• Cardinal.exists_ord_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  (α : Type u_1) : ∃ r, ∃ (x : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r
• Cardinal.ord_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  (α : Type u_1) : ∃ r, ∃ (x : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r
• Ordinal.ord_mk_le_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (s : Set α) : (Cardinal.mk ↑s).ord ≤ Ordinal.type r
• Ordinal.type_nat_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.omega0
• Ordinal.type_ulift 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : Ordinal.type (ULift.down ⁻¹'o r) = Ordinal.lift.{v, u} (Ordinal.type r)
• RelIso.ordinalType_congr 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) : Ordinal.type r = Ordinal.type s
• RelIso.ordinal_type_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) : Ordinal.type r = Ordinal.type s
• Ordinal.inductionOn₂ 📋 Mathlib.SetTheory.Ordinal.Basic
  {motive : Ordinal.{u_1} → Ordinal.{u_2} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop) [inst_1 : IsWellOrder β s], motive (Ordinal.type r) (Ordinal.type s)) : motive o₁ o₂
• Ordinal.type_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type r = Ordinal.type s ↔ Nonempty (r ≃r s)
• RelIso.ordinal_lift_type_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) : Ordinal.lift.{v, u} (Ordinal.type r) = Ordinal.lift.{u, v} (Ordinal.type s)
• Ordinal.top_typein 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (Ordinal.typein r).top = Ordinal.type r
• Ordinal.lift_type_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.lift.{max v w, u} (Ordinal.type r) = Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≃r s)
• InitialSeg.ordinal_type_le 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : InitialSeg r s) : Ordinal.type r ≤ Ordinal.type s
• PrincipalSeg.ordinal_type_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : PrincipalSeg r s) : Ordinal.type r < Ordinal.type s
• RelEmbedding.ordinal_type_le 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (h : r ↪r s) : Ordinal.type r ≤ Ordinal.type s
• Ordinal.ord_mk_lt_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty) : (Cardinal.mk ↑s).ord < Ordinal.type r
• Ordinal.type_le_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (InitialSeg r s)
• Ordinal.type_le_iff' 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type r ≤ Ordinal.type s ↔ Nonempty (r ↪r s)
• Ordinal.type_lt_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type r < Ordinal.type s ↔ Nonempty (PrincipalSeg r s)
• Ordinal.lift_type_le 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.lift.{max v w, u} (Ordinal.type r) ≤ Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (InitialSeg r s)
• Ordinal.lift_type_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : Ordinal.lift.{max v w, u} (Ordinal.type r) < Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (PrincipalSeg r s)
• Ordinal.type_fin 📋 Mathlib.SetTheory.Ordinal.Basic
  (n : ℕ) : (Ordinal.type fun x1 x2 => x1 < x2) = ↑n
• Ordinal.inductionOn₃ 📋 Mathlib.SetTheory.Ordinal.Basic
  {motive : Ordinal.{u_1} → Ordinal.{u_2} → Ordinal.{u_3} → Prop} (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_2}) (o₃ : Ordinal.{u_3}) (type : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsWellOrder α r] (β : Type u_2) (s : β → β → Prop) [inst_1 : IsWellOrder β s] (γ : Type u_3) (t : γ → γ → Prop) [inst_2 : IsWellOrder γ t], motive (Ordinal.type r) (Ordinal.type s) (Ordinal.type t)) : motive o₁ o₂ o₃
• Ordinal.type_preimage 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : Ordinal.type (⇑f ⁻¹'o r) = Ordinal.type r
• Ordinal.type_sum_lex 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type (Sum.Lex r s) = Ordinal.type r + Ordinal.type s
• Ordinal.type_lift_preimage 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : Ordinal.lift.{u, v} (Ordinal.type (⇑f ⁻¹'o r)) = Ordinal.lift.{v, u} (Ordinal.type r)
• Cardinal.ord_eq_Inf 📋 Mathlib.SetTheory.Ordinal.Basic
  (α : Type u) : (Cardinal.mk α).ord = ⨅ r, Ordinal.type ↑r
• Cardinal.ord_eq_iInf 📋 Mathlib.SetTheory.Ordinal.Basic
  (α : Type u) : (Cardinal.mk α).ord = ⨅ r, Ordinal.type ↑r
• Ordinal.inductionOnWellOrder 📋 Mathlib.SetTheory.Ordinal.Basic
  {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}) (type : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], motive (Ordinal.type fun x1 x2 => x1 < x2)) : motive o
• Ordinal.typein_lt_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : (Ordinal.typein r).toRelEmbedding a < Ordinal.type r
• Ordinal.typein_surjOn 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : Set.SurjOn (⇑(Ordinal.typein r).toRelEmbedding) Set.univ (Set.Iio (Ordinal.type r))
• Cardinal.card_typein_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] (x : α) (h : (Cardinal.mk α).ord = Ordinal.type r) : ((Ordinal.typein r).toRelEmbedding x).card < Cardinal.mk α
• Ordinal.enum 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : (fun x1 x2 => x1 < x2) ≃r r
• Ordinal.typein_surj 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r) : o ∈ Set.range ⇑(Ordinal.typein r).toRelEmbedding
• Ordinal.mem_range_typein_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} : o ∈ Set.range ⇑(Ordinal.typein r).toRelEmbedding ↔ o < Ordinal.type r
• Ordinal.typein_top 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg r s) : (Ordinal.typein s).toRelEmbedding f.top = Ordinal.type r
• Ordinal.lift_typein_top 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg r s) : Ordinal.lift.{u, v} ((Ordinal.typein s).toRelEmbedding f.top) = Ordinal.lift.{v, u} (Ordinal.type r)
• Ordinal.type_subrel 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal.type (Subrel r fun x => r x a) = (Ordinal.typein r).toRelEmbedding a
• Ordinal.isSuccPrelimit_type_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] [h : NoMaxOrder α] : Order.IsSuccPrelimit (Ordinal.type fun x1 x2 => x1 < x2)
• Ordinal.isSuccPrelimit_type_lt_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] : Order.IsSuccPrelimit (Ordinal.type fun x1 x2 => x1 < x2) ↔ NoMaxOrder α
• Cardinal.exists_ord_eq_type_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  (α : Type u_1) : ∃ x, ∃ (x_1 : WellFoundedLT α), (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2
• Ordinal.type_lt_mem_range_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] [OrderTop α] : (Ordinal.type fun x1 x2 => x1 < x2) ∈ Set.range Order.succ
• Cardinal.mk_Iio_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] (i : α) (h : (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) : Cardinal.mk ↑(Set.Iio i) < Cardinal.mk α
• Ordinal.type_lt_mem_range_succ_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] : (Ordinal.type fun x1 x2 => x1 < x2) ∈ Set.range Order.succ ↔ ∃ x, IsMax x
• Ordinal.type_lt_ulift 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.lift.{v, u} (Ordinal.type fun x1 x2 => x1 < x2)
• Cardinal.mk_Ioi_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u_1} [LinearOrder α] [WellFoundedGT α] (i : α) (h : (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) : Cardinal.mk ↑(Set.Ioi i) < Cardinal.mk α
• OrderIso.ordinalType_congr 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] [WellFoundedLT β] (h : α ≃o β) : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2
• Ordinal.liftOnWellOrder 📋 Mathlib.SetTheory.Ordinal.Basic
  {δ : Sort v} (o : Ordinal.{u_1}) (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β] [inst_3 : WellFoundedLT β], ((Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2) → f α = f β) : δ
• Ordinal.type_lt_Iio 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u}) : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.lift.{u + 1, u} o
• Ordinal.type_set_le 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] (s : Set α) : (Ordinal.type fun x1 x2 => x1 < x2) ≤ Ordinal.type fun x1 x2 => x1 < x2
• Ordinal.type_toType 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u}) : (Ordinal.type fun x1 x2 => x1 < x2) = o
• Ordinal.enum_zero_le 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] (h0 : 0 < Ordinal.type r) (a : α) : ¬r a ((Ordinal.enum r) ⟨0, h0⟩)
• Ordinal.liftOnWellOrder_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {δ : Sort v} (f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ) (c : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β] [inst_3 : WellFoundedLT β], ((Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2) → f α = f β) {γ : Type u_1} [LinearOrder γ] [WellFoundedLT γ] : (Ordinal.type fun x1 x2 => x1 < x2).liftOnWellOrder f c = f γ
• Ordinal.enum_type 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : PrincipalSeg s r) {h : Ordinal.type s < Ordinal.type r} : (Ordinal.enum r) ⟨Ordinal.type s, h⟩ = f.top
• Ordinal.not_lt_enum_ord_mk_min_compl 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {s : Set α} (hfin : s.Finite) (h : sᶜ.Nonempty) : ¬r ((Ordinal.enum r) ⟨(Cardinal.mk ↑s).ord, ⋯⟩) (⋯.min sᶜ h)
• Ordinal.type_Iio_lt 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] (x : α) : Ordinal.type LT.lt = (Ordinal.typein LT.lt).toRelEmbedding x
• Ordinal.enum_typein 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a : α) : (Ordinal.enum r) ⟨(Ordinal.typein r).toRelEmbedding a, ⋯⟩ = a
• Ordinal.type_mono 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} [LinearOrder α] [WellFoundedLT α] {s t : Set α} (h : s ⊆ t) : (Ordinal.type fun x1 x2 => x1 < x2) ≤ Ordinal.type fun x1 x2 => x1 < x2
• Ordinal.typein_enum 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r) : (Ordinal.typein r).toRelEmbedding ((Ordinal.enum r) ⟨o, h⟩) = o
• Ordinal.enum_symm_apply_coe 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (a✝ : α) : ↑((Ordinal.enum r).symm a✝) = (Ordinal.typein r).toRelEmbedding a✝
• Ordinal.enum_inj 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))} : (Ordinal.enum r) o₁ = (Ordinal.enum r) o₂ ↔ o₁ = o₂
• Ordinal.enum_lt_enum 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))} : r ((Ordinal.enum r) o₁) ((Ordinal.enum r) o₂) ↔ o₁ < o₂
• Ordinal.enum_le_enum 📋 Mathlib.SetTheory.Ordinal.Basic
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))} : ¬r ((Ordinal.enum r) o₁) ((Ordinal.enum r) o₂) ↔ o₂ ≤ o₁
• Ordinal.relIso_enum' 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) (hs : o < Ordinal.type s) : f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.enum s) ⟨o, hs⟩
• Ordinal.relIso_enum 📋 Mathlib.SetTheory.Ordinal.Basic
  {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) : f ((Ordinal.enum r) ⟨o, hr⟩) = (Ordinal.enum s) ⟨o, ⋯⟩
• Ordinal.enum_zero_eq_bot 📋 Mathlib.SetTheory.Ordinal.Basic
  {o : Ordinal.{u_1}} (ho : 0 < o) : (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩ = have H := Ordinal.toTypeOrderBot ⋯; ⊥
• Ordinal.enum_zero_le' 📋 Mathlib.SetTheory.Ordinal.Basic
  {o : Ordinal.{u_1}} (h0 : 0 < o) (a : o.ToType) : (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, ⋯⟩ ≤ a
• Ordinal.one_toType_eq 📋 Mathlib.SetTheory.Ordinal.Basic
  (x : Ordinal.ToType 1) : x = (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, Ordinal.uniqueToTypeOne._proof_2⟩
• Ordinal.le_enum_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  {o : Ordinal.{u_1}} (a : (Order.succ o).ToType) : a ≤ (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ⋯⟩
• Ordinal.enum_le_enum' 📋 Mathlib.SetTheory.Ordinal.Basic
  (a : Ordinal.{u_1}) {o₁ o₂ : ↑(Set.Iio (Ordinal.type fun x1 x2 => x1 < x2))} : (Ordinal.enum fun x1 x2 => x1 < x2) o₁ ≤ (Ordinal.enum fun x1 x2 => x1 < x2) o₂ ↔ o₁ ≤ o₂
• Ordinal.bounded_singleton 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {α : Type u_1} {r : α → α → Prop} [IsWellOrder α r] (hr : Order.IsSuccLimit (Ordinal.type r)) (x : α) : Set.Bounded r {x}
• Ordinal.has_succ_of_type_succ_lt 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {α : Type u_4} {r : α → α → Prop} [wo : IsWellOrder α r] (h : ∀ a < Ordinal.type r, Order.succ a < Ordinal.type r) (x : α) : ∃ y, r x y
• Ordinal.type_prod_lex 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {α β : Type u} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s] : Ordinal.type (Prod.Lex s r) = Ordinal.type r * Ordinal.type s
• Ordinal.enum_lt_nat 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (x : ℕ) : (Ordinal.enum LT.lt) ⟨↑x, ⋯⟩ = x
• Ordinal.enum_lt_fin 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {n : ℕ} (x : Fin n) : (Ordinal.enum LT.lt) ⟨↑↑x, ⋯⟩ = x
• Ordinal.enum_succ_eq_top 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} : (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ⋯⟩ = ⊤
• Ordinal.blsub_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (f : ι → Ordinal.{max u v}) : (Ordinal.type WellOrderingRel).blsub (Ordinal.bfamilyOfFamily f) = Ordinal.lsub f
• Ordinal.bfamilyOfFamily 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} : (ι → α) → (a : Ordinal.{u}) → a < Ordinal.type WellOrderingRel → α
• Ordinal.brange_bfamilyOfFamily 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (f : ι → α) : (Ordinal.type WellOrderingRel).brange (Ordinal.bfamilyOfFamily f) = Set.range f
• Ordinal.bfamilyOfFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (a : Ordinal.{u}) : a < Ordinal.type r → α
• Ordinal.blsub_eq_lsub' 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) : (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = Ordinal.lsub f
• Ordinal.brange_bfamilyOfFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : (Ordinal.type r).brange (Ordinal.bfamilyOfFamily' r f) = Set.range f
• Ordinal.familyOfBFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) : ι → α
• Ordinal.bsup_eq_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}) : (Ordinal.type WellOrderingRel).bsup (Ordinal.bfamilyOfFamily f) = iSup f
• Ordinal.bsup'_eq_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_3} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u_3 u_4}) : (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = iSup f
• Ordinal.blsub_eq_blsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) : (Ordinal.type r).blsub (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').blsub (Ordinal.bfamilyOfFamily' r' f)
• Ordinal.bsup_eq_bsup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) : (Ordinal.type r).bsup (Ordinal.bfamilyOfFamily' r f) = (Ordinal.type r').bsup (Ordinal.bfamilyOfFamily' r' f)
• Ordinal.lsub_eq_blsub' 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u u_3}) : Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = o.blsub f
• Ordinal.range_familyOfBFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) : Set.range (Ordinal.familyOfBFamily' r ho f) = o.brange f
• Ordinal.iSup'_eq_bsup 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_3}} {ι : Type u_3} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : Ordinal.type r = o) (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}) : iSup (Ordinal.familyOfBFamily' r ho f) = o.bsup f
• Ordinal.comp_bfamilyOfFamily 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) : (fun i hi => g (Ordinal.bfamilyOfFamily f i hi)) = Ordinal.bfamilyOfFamily (g ∘ f)
• Ordinal.comp_bfamilyOfFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (g : α → β) : (fun i hi => g (Ordinal.bfamilyOfFamily' r f i hi)) = Ordinal.bfamilyOfFamily' r (g ∘ f)
• Ordinal.lsub_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Ordinal.lsub (Ordinal.familyOfBFamily' r ho f) = Ordinal.lsub (Ordinal.familyOfBFamily' r' ho' f)
• Ordinal.comp_familyOfBFamily' 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β) : g ∘ Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun i hi => g (f i hi)
• Ordinal.iSup_eq_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u_3}) : iSup (Ordinal.familyOfBFamily' r ho f) = iSup (Ordinal.familyOfBFamily' r' ho' f)
• Ordinal.blsub_type 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : (a : Ordinal.{u}) → a < Ordinal.type r → Ordinal.{max u v}) : (Ordinal.type r).blsub f = Ordinal.lsub fun a => f ((Ordinal.typein r).toRelEmbedding a) ⋯
• Ordinal.unbounded_range_of_le_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : Ordinal.type r ≤ ⨆ i, (Ordinal.typein r).toRelEmbedding (f i)) : Set.Unbounded r (Set.range f)
• Ordinal.familyOfBFamily'_enum 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (i : Ordinal.{u}) (hi : i < o) : Ordinal.familyOfBFamily' r ho f ((Ordinal.enum r) ⟨i, ⋯⟩) = f i hi
• Ordinal.familyOfBFamily_enum 📋 Mathlib.SetTheory.Ordinal.Family
  {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → a < o → α) (i : Ordinal.{u_3}) (hi : i < o) : o.familyOfBFamily f ((Ordinal.enum fun x1 x2 => x1 < x2) ⟨i, ⋯⟩) = f i hi
• Ordinal.type_lt_ordinal 📋 Mathlib.SetTheory.Ordinal.Univ
  : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
• Ordinal.univ_id 📋 Mathlib.SetTheory.Ordinal.Univ
  : Ordinal.univ.{u, u + 1} = Ordinal.type fun x1 x2 => x1 < x2
• Ordinal.liftPrincipalSeg_top' 📋 Mathlib.SetTheory.Ordinal.Univ
  : Ordinal.liftPrincipalSeg.top = Ordinal.type fun x1 x2 => x1 < x2
• Cardinal.ord_cardinalMk 📋 Mathlib.SetTheory.Cardinal.Cofinality.Enum
  {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] : (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2
• Order.ord_cof_eq_type_lt 📋 Mathlib.SetTheory.Cardinal.Cofinality.Enum
  {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] : (Order.cof α).ord = Ordinal.type fun x1 x2 => x1 < x2
• IsRegularCardinalOrder.mk 📋 Mathlib.SetTheory.Cardinal.Cofinality.Enum
  {α : Type u_2} [LinearOrder α] [WellFoundedLT α] (type_lt_le_ord_cof : (Ordinal.type fun x1 x2 => x1 < x2) ≤ (Order.cof α).ord) : IsRegularCardinalOrder α
• IsRegularCardinalOrder.type_lt_le_ord_cof 📋 Mathlib.SetTheory.Cardinal.Cofinality.Enum
  {α : Type u_2} {inst✝ : LinearOrder α} {inst✝¹ : WellFoundedLT α} [self : IsRegularCardinalOrder α] : (Ordinal.type fun x1 x2 => x1 < x2) ≤ (Order.cof α).ord
• Order.type_eq_of_isCofinal 📋 Mathlib.SetTheory.Cardinal.Cofinality.Enum
  {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} (hs : IsCofinal s) : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2
• Cardinal.type_cardinal 📋 Mathlib.SetTheory.Cardinal.Aleph
  : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
• Ordinal.type_lt_cardinal 📋 Mathlib.SetTheory.Cardinal.Aleph
  : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
• Cardinal.mk_Iic_lt 📋 Mathlib.SetTheory.Cardinal.Arithmetic
  {α : Type u_1} [LinearOrder α] [WellFoundedLT α] (i : α) (h : (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) (hα : Cardinal.aleph0 ≤ Cardinal.mk α) : Cardinal.mk ↑(Set.Iic i) < Cardinal.mk α
• Cardinal.mk_Ici_lt 📋 Mathlib.SetTheory.Cardinal.Arithmetic
  {α : Type u_1} [LinearOrder α] [WellFoundedGT α] (i : α) (h : (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2) (hα : Cardinal.aleph0 ≤ Cardinal.mk α) : Cardinal.mk ↑(Set.Ici i) < Cardinal.mk α
• Cardinal.mk_bounded_subset 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {α : Type u_1} (h : (Cardinal.mk α).IsStrongPrelimit) {r : α → α → Prop} [IsWellOrder α r] (hr : (Cardinal.mk α).ord = Ordinal.type r) : Cardinal.mk { s // Set.Bounded r s } = Cardinal.mk α
• Ordinal.cof_eq' 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {α : Type u} (r : α → α → Prop) [H : IsWellOrder α r] (h : Order.IsSuccLimit (Ordinal.type r)) : ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ Cardinal.mk ↑S = (Ordinal.type r).cof
• Ordinal.cof_type 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  (α : Type u_1) [LinearOrder α] [WellFoundedLT α] : (Ordinal.type fun x1 x2 => x1 < x2).cof = Order.cof α
• Ordinal.exists_ord_cof_eq 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  (α : Type u) [LinearOrder α] [WellFoundedLT α] : ∃ s, IsCofinal s ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
• Ordinal.ord_cof_eq 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  (α : Type u) [LinearOrder α] [WellFoundedLT α] : ∃ s, IsCofinal s ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
• Ordinal.exists_ord_cof_eq_of_isCofinal 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {α : Type u} [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : ∃ t ⊆ s, IsCofinal t ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
• Profinite.NobelingProof.term 📋 Mathlib.Topology.Category.Profinite.Nobeling.Basic
  (I : Type u) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : I
• Profinite.NobelingProof.ord_term_aux 📋 Mathlib.Topology.Category.Profinite.Nobeling.Basic
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.ord I (Profinite.NobelingProof.term I ho) = o
• Profinite.NobelingProof.term_ord_aux 📋 Mathlib.Topology.Category.Profinite.Nobeling.Basic
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {i : I} (ho : Profinite.NobelingProof.ord I i < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.term I ho = i
• Profinite.NobelingProof.ord_term 📋 Mathlib.Topology.Category.Profinite.Nobeling.Basic
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (i : I) : Profinite.NobelingProof.ord I i = o ↔ Profinite.NobelingProof.term I ho = i
• Profinite.NobelingProof.C' 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set (I → Bool)
• Profinite.NobelingProof.C0 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set (I → Bool)
• Profinite.NobelingProof.C1 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set (I → Bool)
• Profinite.NobelingProof.GoodProducts.MaxProducts 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set (Profinite.NobelingProof.Products I)
• Profinite.NobelingProof.contained_C' 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.contained (Profinite.NobelingProof.C' C ho) o
• Profinite.NobelingProof.CC'₀ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : ↑(Profinite.NobelingProof.C' C ho) → ↑C
• Profinite.NobelingProof.swapTrue_eq_true 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (x : I → Bool) : Profinite.NobelingProof.SwapTrue o x (Profinite.NobelingProof.term I ho) = true
• Profinite.NobelingProof.CC'₁ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : ↑(Profinite.NobelingProof.C' C ho) → ↑C
• Profinite.NobelingProof.isClosed_C' 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : IsClosed (Profinite.NobelingProof.C' C ho)
• Profinite.NobelingProof.isClosed_C0 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : IsClosed (Profinite.NobelingProof.C0 C ho)
• Profinite.NobelingProof.isClosed_C1 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : IsClosed (Profinite.NobelingProof.C1 C ho)
• Profinite.NobelingProof.union_C0C1_eq 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.C0 C ho ∪ Profinite.NobelingProof.C1 C ho = C
• Profinite.NobelingProof.mem_C'_eq_false 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (x : I → Bool) : x ∈ Profinite.NobelingProof.C' C ho → x (Profinite.NobelingProof.term I ho) = false
• Profinite.NobelingProof.contained_C1 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.contained (Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o) o
• Profinite.NobelingProof.GoodProducts.sum_to 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → Profinite.NobelingProof.Products I
• Profinite.NobelingProof.GoodProducts.injective_sum_to 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Function.Injective (Profinite.NobelingProof.GoodProducts.sum_to C ho)
• Profinite.NobelingProof.C0_projOrd 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) {x : I → Bool} (hx : x ∈ Profinite.NobelingProof.C0 C ho) : Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x = x
• Profinite.NobelingProof.C1_projOrd 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) {x : I → Bool} (hx : x ∈ Profinite.NobelingProof.C1 C ho) : Profinite.NobelingProof.SwapTrue o (Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x) = x
• Profinite.NobelingProof.GoodProducts.sum_equiv 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) ≃ ↑(Profinite.NobelingProof.GoodProducts C)
• Profinite.NobelingProof.GoodProducts.union_succ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.GoodProducts C = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho
• Profinite.NobelingProof.continuous_CC'₀ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Continuous (Profinite.NobelingProof.CC'₀ C ho)
• Profinite.NobelingProof.GoodProducts.SumEval 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → LocallyConstant ↑C ℤ
• Profinite.NobelingProof.continuous_CC'₁ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Continuous (Profinite.NobelingProof.CC'₁ C hsC ho)
• Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [Inhabited I] (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : (↑↑l).head! = Profinite.NobelingProof.term I ho
• Profinite.NobelingProof.GoodProducts.sum_to_range 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set.range (Profinite.NobelingProof.GoodProducts.sum_to C ho) = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho
• Profinite.NobelingProof.swapTrue_mem_C1 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (f : ↑(Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o)) : Profinite.NobelingProof.SwapTrue o ↑f ∈ Profinite.NobelingProof.C1 C ho
• Profinite.NobelingProof.Products.max_eq_o_cons_tail 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) : ↑l = Profinite.NobelingProof.term I ho :: ↑l.Tail
• Profinite.NobelingProof.GoodProducts.isChain_cons_of_lt 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) (q : Profinite.NobelingProof.Products I) (hq : q < (↑l).Tail) : List.IsChain (fun x x_1 => x > x_1) (Profinite.NobelingProof.term I ho :: ↑q)
• Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : ↑↑l = Profinite.NobelingProof.term I ho :: ↑(↑l).Tail
• Profinite.NobelingProof.Products.max_eq_o_cons_tail' 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) (hlc : List.IsChain (fun x1 x2 => x1 > x2) (Profinite.NobelingProof.term I ho :: ↑l.Tail)) : l = ⟨Profinite.NobelingProof.term I ho :: ↑l.Tail, hlc⟩
• Profinite.NobelingProof.GoodProducts.good_lt_maxProducts 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (q : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l
• Profinite.NobelingProof.Linear_CC'₀ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
• Profinite.NobelingProof.Linear_CC' 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
• Profinite.NobelingProof.Linear_CC'₁ 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
• Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.SumEval C ho)
• Profinite.NobelingProof.GoodProducts.span_sum 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Set.range (Profinite.NobelingProof.GoodProducts.eval C) = Set.range (Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l)
• Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.GoodProducts.eval C ∘ (Profinite.NobelingProof.GoodProducts.sum_equiv C hsC ho).toFun = Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l
• Profinite.NobelingProof.GoodProducts.max_eq_eval 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C ↑l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
• Profinite.NobelingProof.Products.max_eq_eval 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) : (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) l.Tail
• Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : (⇑(Profinite.NobelingProof.Linear_CC' C hsC ho) ∘ fun l => Profinite.NobelingProof.Products.eval C ↑l) = fun l => Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
• Profinite.NobelingProof.succ_exact 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ), X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ), f := ModuleCat.ofHom (Profinite.NobelingProof.πs C o), g := ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho), zero := ⋯ }.Exact
• Profinite.NobelingProof.CC_comp_zero 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (y : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ) : (Profinite.NobelingProof.Linear_CC' C hsC ho) ((Profinite.NobelingProof.πs C o) y) = 0
• Profinite.NobelingProof.CC_exact 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) {f : LocallyConstant ↑C ℤ} (hf : (Profinite.NobelingProof.Linear_CC' C hsC ho) f = 0) : ∃ y, (Profinite.NobelingProof.πs C o) y = f
• Profinite.NobelingProof.GoodProducts.MaxToGood 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))) : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.C' C ho))
• Profinite.NobelingProof.GoodProducts.maxToGood_injective 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))) : Function.Injective (Profinite.NobelingProof.GoodProducts.MaxToGood C hC hsC ho h₁)
• Profinite.NobelingProof.GoodProducts.maxTail_isGood 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))) : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.C' C ho) (↑l).Tail
• Profinite.NobelingProof.GoodProducts.square_commutes 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun x1 x2 => x1 < x2) : Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Profinite.NobelingProof.πs C o))) ∘ Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
• Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval 📋 Mathlib.Topology.Category.Profinite.Nobeling.Successor
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.C' C ho)) → LinearIndependent (ι := ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) ℤ (⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho))) ∘ Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inr)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59