Loogle!

Result

Found 171 declarations mentioning Order.succ and Ordinal.

• Ordinal.succ_ne_zero 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u_1}) : Order.succ o ≠ 0
• Cardinal.lt_ord_succ_card 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u_1}) : o < (Order.succ o.card).ord
• Ordinal.succ_zero 📋 Mathlib.SetTheory.Ordinal.Basic
  : Order.succ 0 = 1
• Ordinal.succ_pos 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u_1}) : 0 < Order.succ o
• Ordinal.natCast_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  (n : ℕ) : ↑n.succ = Order.succ ↑n
• Ordinal.add_one_eq_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u_1}) : o + 1 = Order.succ o
• Cardinal.card_le_iff 📋 Mathlib.SetTheory.Ordinal.Basic
  {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} : o.card ≤ c ↔ o < (Order.succ c).ord
• Ordinal.card_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  (o : Ordinal.{u_1}) : (Order.succ o).card = o.card + 1
• Ordinal.add_succ 📋 Mathlib.SetTheory.Ordinal.Basic
  (o₁ o₂ : Ordinal.{u_1}) : o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)
• Ordinal.succ_one 📋 Mathlib.SetTheory.Ordinal.Basic
  : Order.succ 1 = 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.pred_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (o : Ordinal.{u_4}) : (Order.succ o).pred = o
• Ordinal.pred_succ_gi 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  : GaloisInsertion Ordinal.pred Order.succ
• Ordinal.self_le_succ_pred 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (o : Ordinal.{u_4}) : o ≤ Order.succ o.pred
• Ordinal.lift_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (a : Ordinal.{v}) : Ordinal.lift.{u, v} (Order.succ a) = Order.succ (Ordinal.lift.{u, v} a)
• Ordinal.succ_pred_eq_iff_not_isSuccPrelimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} : Order.succ o.pred = o ↔ ¬Order.IsSuccPrelimit o
• Ordinal.lt_pred_iff_succ_lt 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} : a < b.pred ↔ Order.succ a < b
• Ordinal.pred_le_iff_le_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} : a.pred ≤ b ↔ a ≤ Order.succ b
• Ordinal.one_add_natCast 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (m : ℕ) : 1 + ↑m = ↑(Order.succ m)
• Ordinal.zero_or_succ_or_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (o : Ordinal.{u_4}) : o = 0 ∨ o ∈ Set.range Order.succ ∨ Order.IsSuccLimit o
• Ordinal.limitRecOn 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {motive : Ordinal.{u_5} → Sort u_4} (o : Ordinal.{u_5}) (zero : motive 0) (succ : (o : Ordinal.{u_5}) → motive o → motive (Order.succ o)) (limit : (o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) : motive o
• Ordinal.one_add_ofNat 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (m : ℕ) [m.AtLeastTwo] : 1 + OfNat.ofNat m = Order.succ (OfNat.ofNat m)
• 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.lt_mul_succ_div 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b ≠ 0) : a < b * Order.succ (a / b)
• Ordinal.mul_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (a b : Ordinal.{u_4}) : a * Order.succ b = a * b + a
• Ordinal.toType_noMax_of_succ_lt 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} (ho : ∀ a < o, Order.succ a < o) : NoMaxOrder o.ToType
• Ordinal.div_le 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * Order.succ c
• Ordinal.lt_div 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (h : c ≠ 0) : a < b / c ↔ c * Order.succ a ≤ b
• Ordinal.limitRecOn_zero 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {motive : Ordinal.{u_4} → Sort u_5} (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) : Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁
• Ordinal.limitRecOn_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) : Ordinal.limitRecOn (Order.succ o) H₁ H₂ H₃ = H₂ o (Ordinal.limitRecOn o H₁ H₂ H₃)
• Ordinal.orderTopToTypeSucc 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (o : Ordinal.{u_4}) : OrderTop (Order.succ o).ToType
• Ordinal.add_mul_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (c : Ordinal.{u_4}) (ba : b + a = a) : (a + b) * Order.succ c = a * Order.succ c + b
• Ordinal.limitRecOn_limit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0) (H₂ : (o : Ordinal.{u_4}) → motive o → motive (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) (h : Order.IsSuccLimit o) : Ordinal.limitRecOn o H₁ H₂ H₃ = H₃ o h fun x _h => Ordinal.limitRecOn x H₁ H₂ H₃
• Ordinal.boundedLimitRecOn 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {l : Ordinal.{u_5}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_4} (o : ↑(Set.Iio l)) (zero : motive ⟨0, ⋯⟩) (succ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (limit : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : motive o
• Ordinal.boundedLimitRec_zero 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : Ordinal.boundedLimitRecOn lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁
• Ordinal.boundedLimitRec_limit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) (oLim : Order.IsSuccLimit ↑o) : Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun x x_1 => Ordinal.boundedLimitRecOn lLim x H₁ H₂ H₃
• Ordinal.boundedLimitRec_succ 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {l : Ordinal.{u_4}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_5} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : Ordinal.boundedLimitRecOn lLim ⟨Order.succ ↑o, ⋯⟩ H₁ H₂ H₃ = H₂ o (Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃)
• Ordinal.boundedLimitRecOn.eq_1 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {l : Ordinal.{u_5}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_4} (o : ↑(Set.Iio l)) (zero : motive ⟨0, ⋯⟩) (succ : (o : ↑(Set.Iio l)) → motive o → motive ⟨Order.succ ↑o, ⋯⟩) (limit : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : Ordinal.boundedLimitRecOn lLim o zero succ limit = Ordinal.limitRecOn (motive := fun p => (h : p < l) → motive ⟨p, h⟩) (↑o) (fun x => zero) (fun o ih h => succ ⟨o, ⋯⟩ (ih ⋯)) (fun _o ho ih x => limit ⟨_o, x⟩ ho fun _o' h => ih (↑_o') h ⋯) ⋯
• Ordinal.enum_succ_eq_top 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} : (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ⋯⟩ = ⊤
• Ordinal.lsub_const 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} [Nonempty ι] (o : Ordinal.{max u_5 u_4}) : (Ordinal.lsub fun x => o) = Order.succ o
• Ordinal.lsub_unique 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4}) : Ordinal.lsub f = Order.succ (f default)
• Ordinal.bsup_id_succ 📋 Mathlib.SetTheory.Ordinal.Family
  (o : Ordinal.{u}) : ((Order.succ o).bsup fun x x_1 => x) = o
• Ordinal.iSup_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup (Order.succ ∘ f) = Ordinal.lsub f
• Ordinal.sup_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup (Order.succ ∘ f) = Ordinal.lsub f
• Ordinal.lsub_le_succ_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Ordinal.lsub f ≤ Order.succ (iSup f)
• Ordinal.lsub_le_sup_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Ordinal.lsub f ≤ Order.succ (iSup f)
• Ordinal.blsub_le_bsup_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.blsub f ≤ Order.succ (o.bsup f)
• Ordinal.blsub_const 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) : (o.blsub fun x x_1 => a) = Order.succ a
• Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f = o.blsub f ∨ Order.succ (o.bsup f) = o.blsub f
• Ordinal.sInf_compl_lt_ord_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (f : ι → Ordinal.{u}) : sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord
• Ordinal.bsup_eq_blsub 📋 Mathlib.SetTheory.Ordinal.Family
  (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : (o.bsup fun a ha => Order.succ (f a ha)) = o.blsub f
• Ordinal.sInf_compl_lt_lift_ord_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u} (f : ι → Ordinal.{max u v}) : sInf (Set.range f)ᶜ < Ordinal.lift.{v, u} (Order.succ (Cardinal.mk ι)).ord
• Ordinal.bsup_id_limit 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} : (∀ a < o, Order.succ a < o) → (o.bsup fun x x_1 => x) = o
• Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup f = Ordinal.lsub f ∨ Order.succ (iSup f) = Ordinal.lsub f
• Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup f = Ordinal.lsub f ∨ Order.succ (iSup f) = Ordinal.lsub f
• Ordinal.succ_iSup_eq_lsub_iff 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Order.succ (iSup f) = Ordinal.lsub f ↔ ∃ i, f i = iSup f
• Ordinal.sup_succ_eq_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Order.succ (iSup f) = Ordinal.lsub f ↔ ∃ i, f i = iSup f
• Ordinal.blsub_one 📋 Mathlib.SetTheory.Ordinal.Family
  (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}) : Ordinal.blsub 1 f = Order.succ (f 0 ⋯)
• Ordinal.iSup_eq_lsub_iff 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f
• Ordinal.succ_iSup_le_lsub_iff 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Order.succ (iSup f) ≤ Ordinal.lsub f ↔ ∃ i, f i = iSup f
• Ordinal.sup_eq_lsub_iff_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : iSup f = Ordinal.lsub f ↔ ∀ a < Ordinal.lsub f, Order.succ a < Ordinal.lsub f
• Ordinal.sup_succ_le_lsub 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Order.succ (iSup f) ≤ Ordinal.lsub f ↔ ∃ i, f i = iSup f
• Ordinal.bsup_eq_blsub_iff_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, Order.succ a < o.blsub f
• Ordinal.isNormal_iff_lt_succ_and_blsub_eq 📋 Mathlib.SetTheory.Ordinal.Family
  {f : Ordinal.{u} → Ordinal.{max u v}} : Order.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.blsub fun x x_1 => f x) = f o
• Ordinal.isNormal_iff_lt_succ_and_bsup_eq 📋 Mathlib.SetTheory.Ordinal.Family
  {f : Ordinal.{u} → Ordinal.{max u v}} : Order.IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.bsup fun x x_1 => f x) = f o
• Ordinal.bsup_succ_eq_blsub 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Order.succ (o.bsup f) = o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
• Ordinal.bsup_not_succ_of_ne_bsup 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f) (a : Ordinal.{max u v}) : a < o.bsup f → Order.succ a < o.bsup f
• Ordinal.bsup_eq_blsub_of_lt_succ_limit 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} (hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ⋯) : o.bsup f = o.blsub f
• Ordinal.bsup_succ_le_blsub 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ i, ∃ (hi : i < o), f i hi = o.bsup f
• Ordinal.IsNormal.eq_iff_zero_and_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {f g : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hg : Order.IsNormal g) : f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)
• Ordinal.succ_lt_iSup_of_ne_iSup 📋 Mathlib.SetTheory.Ordinal.Family
  {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] (hf : ∀ (i : ι), f i ≠ iSup f) {a : Ordinal.{u}} (hao : a < iSup f) : Order.succ a < iSup f
• Ordinal.bsup_succ_of_mono 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < Order.succ o → Ordinal.{max u_4 u_5}} (hf : ∀ {i j : Ordinal.{u_4}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) : (Order.succ o).bsup f = f o ⋯
• Ordinal.blsub_succ_of_mono 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < Order.succ o → Ordinal.{max u v}} (hf : ∀ {i j : Ordinal.{u}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) : (Order.succ o).blsub f = Order.succ (f o ⋯)
• Ordinal.lt_bsup_of_limit 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}} (hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') (ho : ∀ a < o, Order.succ a < o) (i : Ordinal.{u_4}) (h : i < o) : f i h < o.bsup f
• Ordinal.iSup_typein_limit 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) : iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
• Ordinal.sup_typein_limit 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) : iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
• Ordinal.iSup_typein_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_4}} : iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
• Ordinal.sup_typein_succ 📋 Mathlib.SetTheory.Ordinal.Family
  {o : Ordinal.{u_4}} : iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
• Ordinal.enumOrd_succ_le 📋 Mathlib.SetTheory.Ordinal.Enum
  {a b : Ordinal.{u}} {s : Set Ordinal.{u}} (hs : ¬BddAbove s) (ha : a ∈ s) (hb : Ordinal.enumOrd s b < a) : Ordinal.enumOrd s (Order.succ b) ≤ a
• Ordinal.isInitial_succ 📋 Mathlib.SetTheory.Cardinal.Aleph
  {o : Ordinal.{u_1}} : (Order.succ o).IsInitial ↔ o < Ordinal.omega0
• Cardinal.succ_aleph0 📋 Mathlib.SetTheory.Cardinal.Aleph
  : Order.succ Cardinal.aleph0 = Cardinal.aleph 1
• Cardinal.beth_succ 📋 Mathlib.SetTheory.Cardinal.Aleph
  (o : Ordinal.{u_1}) : Cardinal.beth (Order.succ o) = 2 ^ Cardinal.beth o
• Cardinal.preBeth_succ 📋 Mathlib.SetTheory.Cardinal.Aleph
  (o : Ordinal.{u_1}) : Cardinal.preBeth (Order.succ o) = 2 ^ Cardinal.preBeth o
• Cardinal.aleph_succ 📋 Mathlib.SetTheory.Cardinal.Aleph
  (o : Ordinal.{u_1}) : Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)
• Cardinal.preAleph_succ 📋 Mathlib.SetTheory.Cardinal.Aleph
  (o : Ordinal.{u_1}) : Cardinal.preAleph (Order.succ o) = Order.succ (Cardinal.preAleph o)
• Ordinal.lt_opow_succ_log_self 📋 Mathlib.SetTheory.Ordinal.Exponential
  {b : Ordinal.{u_1}} (hb : 1 < b) (x : Ordinal.{u_1}) : x < b ^ Order.succ (Ordinal.log b x)
• Ordinal.opow_succ 📋 Mathlib.SetTheory.Ordinal.Exponential
  (a b : Ordinal.{u_1}) : a ^ Order.succ b = a ^ b * a
• Ordinal.opow_lt_opow_left_of_succ 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b c : Ordinal.{u_1}} (ab : a < b) : a ^ Order.succ c < b ^ Order.succ c
• Ordinal.succ_log_def 📋 Mathlib.SetTheory.Ordinal.Exponential
  {b x : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) : Order.succ (Ordinal.log b x) = sInf {o | x < b ^ o}
• Ordinal.lt_omega0_opow_succ 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b : Ordinal.{u_1}} : a < Ordinal.omega0 ^ Order.succ b ↔ ∃ n, a < Ordinal.omega0 ^ b * ↑n
• Ordinal.log_eq_iff 📋 Mathlib.SetTheory.Ordinal.Exponential
  {b x : Ordinal.{u_1}} (hb : 1 < b) (hx : x ≠ 0) (y : Ordinal.{u_1}) : Ordinal.log b x = y ↔ b ^ y ≤ x ∧ x < b ^ Order.succ y
• Ordinal.opow_mul_add_lt_opow_succ 📋 Mathlib.SetTheory.Ordinal.Exponential
  {b u v w : Ordinal.{u_1}} (hvb : v < b) (hw : w < b ^ u) : b ^ u * v + w < b ^ Order.succ u
• Ordinal.opow_mul_add_lt_opow_mul_succ 📋 Mathlib.SetTheory.Ordinal.Exponential
  {b u w : Ordinal.{u_1}} (v : Ordinal.{u_1}) (hw : w < b ^ u) : b ^ u * v + w < b ^ u * Order.succ v
• Ordinal.deriv_succ 📋 Mathlib.SetTheory.Ordinal.FixedPoint
  (f : Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}) : Ordinal.deriv f (Order.succ o) = Ordinal.nfp f (Order.succ (Ordinal.deriv f o))
• Ordinal.derivFamily_succ 📋 Mathlib.SetTheory.Ordinal.FixedPoint
  {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}) (o : Ordinal.{u_2}) : Ordinal.derivFamily f (Order.succ o) = Ordinal.nfpFamily f (Order.succ (Ordinal.derivFamily f o))
• Ordinal.nfp_mul_opow_omega0_add 📋 Mathlib.SetTheory.Ordinal.FixedPoint
  {a c : Ordinal.{u_1}} (b : Ordinal.{u_1}) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ a ^ Ordinal.omega0) : Ordinal.nfp (fun x => a * x) (a ^ Ordinal.omega0 * b + c) = a ^ Ordinal.omega0 * Order.succ b
• Ordinal.cof_succ 📋 Mathlib.SetTheory.Cardinal.Cofinality
  (o : Ordinal.{u_1}) : (Order.succ o).cof = 1
• Ordinal.cof_eq_one_iff_is_succ 📋 Mathlib.SetTheory.Cardinal.Cofinality
  {o : Ordinal.{u}} : o.cof = 1 ↔ ∃ a, o = Order.succ a
• Ordinal.IsFundamentalSequence.succ 📋 Mathlib.SetTheory.Cardinal.Cofinality
  {o : Ordinal.{u}} : (Order.succ o).IsFundamentalSequence 1 fun x x_1 => o
• Cardinal.isRegular_aleph_succ 📋 Mathlib.SetTheory.Cardinal.Regular
  (o : Ordinal.{u_1}) : (Cardinal.aleph (Order.succ o)).IsRegular
• Cardinal.isRegular_preAleph_succ 📋 Mathlib.SetTheory.Cardinal.Regular
  {o : Ordinal.{u_1}} (h : Ordinal.omega0 ≤ o) : (Cardinal.preAleph (Order.succ o)).IsRegular
• Ordinal.mul_eq_opow_log_succ 📋 Mathlib.SetTheory.Ordinal.Principal
  {a b : Ordinal.{u}} (ha : a ≠ 0) (hb : Ordinal.Principal (fun x1 x2 => x1 * x2) b) (hb₂ : 2 < b) : a * b = b ^ Order.succ (Ordinal.log b a)
• IsWellFounded.rank_eq 📋 Mathlib.SetTheory.Ordinal.Rank
  {α : Type u} (r : α → α → Prop) [hwf : IsWellFounded α r] (a : α) : IsWellFounded.rank r a = ⨆ b, Order.succ (IsWellFounded.rank r ↑b)
• Acc.rank_eq 📋 Mathlib.SetTheory.Ordinal.Rank
  {α : Type u} {a : α} {r : α → α → Prop} (h : Acc r a) : h.rank = ⨆ b, Order.succ ⋯.rank
• Ordinal.nadd_one 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a : Ordinal.{u_1}) : a.nadd 1 = Order.succ a
• Ordinal.nmul_succ 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u_1}) : a.nmul (Order.succ b) = (a.nmul b).nadd a
• Ordinal.one_nadd 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a : Ordinal.{u}) : Ordinal.nadd 1 a = Order.succ a
• Ordinal.succ_nmul 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u_1}) : (Order.succ a).nmul b = (a.nmul b).nadd b
• Ordinal.nadd_succ 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u}) : a.nadd (Order.succ b) = Order.succ (a.nadd b)
• Ordinal.succ_nadd 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u}) : (Order.succ a).nadd b = Order.succ (a.nadd b)
• Ordinal.nadd.eq_1 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u}) : a.nadd b = max (⨆ x, Order.succ ((↑x).nadd b)) (⨆ x, Order.succ (a.nadd ↑x))
• Ordinal.nadd.eq_def 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a b : Ordinal.{u}) : a.nadd b = max (⨆ x, Order.succ ((↑x).nadd b)) (⨆ x, Order.succ (a.nadd ↑x))
• NatOrdinal.succ_def 📋 Mathlib.SetTheory.Ordinal.NaturalOps
  (a : NatOrdinal) : Order.succ a = Ordinal.toNatOrdinal (NatOrdinal.toOrdinal a + 1)
• Nimber.succ_def 📋 Mathlib.SetTheory.Nimber.Basic
  (a : Nimber) : Order.succ a = Ordinal.toNimber (Nimber.toOrdinal a + 1)
• OrdinalApprox.exists_gfpApprox_eq_gfpApprox 📋 Mathlib.SetTheory.Ordinal.FixedPointApproximants
  {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) : ∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.gfpApprox f x a = OrdinalApprox.gfpApprox f x b
• OrdinalApprox.exists_lfpApprox_eq_lfpApprox 📋 Mathlib.SetTheory.Ordinal.FixedPointApproximants
  {α : Type u} [CompleteLattice α] (f : α →o α) (x : α) : ∃ a < (Order.succ (Cardinal.mk α)).ord, ∃ b < (Order.succ (Cardinal.mk α)).ord, a ≠ b ∧ OrdinalApprox.lfpApprox f x a = OrdinalApprox.lfpApprox f x b
• ONote.fundamentalSequenceProp_inl_some 📋 Mathlib.SetTheory.Ordinal.Notation
  (o a : ONote) : o.FundamentalSequenceProp (Sum.inl (some a)) ↔ o.repr = Order.succ a.repr ∧ (o.NF → a.NF)
• ONote.FundamentalSequenceProp.eq_2 📋 Mathlib.SetTheory.Ordinal.Notation
  (o a : ONote) : o.FundamentalSequenceProp (Sum.inl (some a)) = (o.repr = Order.succ a.repr ∧ (o.NF → a.NF))
• ONote.repr_opow_aux₂ 📋 Mathlib.SetTheory.Ordinal.Notation
  {a0 a' : ONote} [N0 : a0.NF] [Na' : a'.NF] (m : ℕ) (d : Ordinal.omega0 ∣ a'.repr) (e0 : a0.repr ≠ 0) (h : a'.repr + ↑m < Ordinal.omega0 ^ a0.repr) (n : ℕ+) (k : ℕ) : have R := (ONote.opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr; (k ≠ 0 → R < (Ordinal.omega0 ^ a0.repr) ^ Order.succ ↑k) ∧ (Ordinal.omega0 ^ a0.repr) ^ ↑k * (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr) + R = (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ Order.succ ↑k
• Ordinal.veblen_succ 📋 Mathlib.SetTheory.Ordinal.Veblen
  (o : Ordinal.{u_1}) : Ordinal.veblen (Order.succ o) = Ordinal.deriv (Ordinal.veblen o)
• Ordinal.veblenWith_succ 📋 Mathlib.SetTheory.Ordinal.Veblen
  {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) : Ordinal.veblenWith f (Order.succ o) = Ordinal.deriv (Ordinal.veblenWith f o)
• Ordinal.gamma_succ_eq_nfp 📋 Mathlib.SetTheory.Ordinal.Veblen
  (o : Ordinal.{u_1}) : (Order.succ o).gamma = Ordinal.nfp (fun x => Ordinal.veblen x 0) (Order.succ o.gamma)
• Ordinal.epsilon_succ_eq_nfp 📋 Mathlib.SetTheory.Ordinal.Veblen
  (o : Ordinal.{u_1}) : (Order.succ o).epsilon = Ordinal.nfp (fun a => Ordinal.omega0 ^ a) (Order.succ o.epsilon)
• PSet.rank_powerset 📋 Mathlib.SetTheory.ZFC.Rank
  (x : PSet.{u_1}) : x.powerset.rank = Order.succ x.rank
• ZFSet.rank_powerset 📋 Mathlib.SetTheory.ZFC.Rank
  (x : ZFSet.{u_1}) : x.powerset.rank = Order.succ x.rank
• PSet.rank_singleton 📋 Mathlib.SetTheory.ZFC.Rank
  (x : PSet.{u_1}) : {x}.rank = Order.succ x.rank
• ZFSet.rank_singleton 📋 Mathlib.SetTheory.ZFC.Rank
  (x : ZFSet.{u_1}) : {x}.rank = Order.succ x.rank
• PSet.le_succ_rank_sUnion 📋 Mathlib.SetTheory.ZFC.Rank
  (x : PSet.{u_1}) : x.rank ≤ Order.succ (⋃₀ x).rank
• ZFSet.le_succ_rank_sUnion 📋 Mathlib.SetTheory.ZFC.Rank
  (x : ZFSet.{u_1}) : x.rank ≤ Order.succ x.sUnion.rank
• PSet.rank.eq_1 📋 Mathlib.SetTheory.ZFC.Rank
  (α : Type u) (A : α → PSet.{u}) : (PSet.mk α A).rank = ⨆ a, Order.succ (A a).rank
• ZFSet.rank_range 📋 Mathlib.SetTheory.ZFC.Rank
  {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : (ZFSet.range f).rank = ⨆ i, Order.succ (f i).rank
• PSet.rank.eq_def 📋 Mathlib.SetTheory.ZFC.Rank
  (x✝ : PSet.{u}) : x✝.rank = match x✝ with | PSet.mk α A => ⨆ a, Order.succ (A a).rank
• PSet.rank_insert 📋 Mathlib.SetTheory.ZFC.Rank
  (x y : PSet.{u_1}) : (insert x y).rank = max (Order.succ x.rank) y.rank
• ZFSet.rank_insert 📋 Mathlib.SetTheory.ZFC.Rank
  (x y : ZFSet.{u_1}) : (insert x y).rank = max (Order.succ x.rank) y.rank
• PSet.rank_pair 📋 Mathlib.SetTheory.ZFC.Rank
  (x y : PSet.{u_1}) : {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
• ZFSet.rank_pair 📋 Mathlib.SetTheory.ZFC.Rank
  (x y : ZFSet.{u_1}) : {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
• Ordinal.toZFSet_succ 📋 Mathlib.SetTheory.ZFC.Ordinal
  (o : Ordinal.{u_1}) : (Order.succ o).toZFSet = insert o.toZFSet o.toZFSet
• ZFSet.vonNeumann_succ 📋 Mathlib.SetTheory.ZFC.VonNeumann
  (o : Ordinal.{u_1}) : ZFSet.vonNeumann (Order.succ o) = (ZFSet.vonNeumann o).powerset
• ZFSet.mem_vonNeumann_succ 📋 Mathlib.SetTheory.ZFC.VonNeumann
  (x : ZFSet.{u_1}) : x ∈ ZFSet.vonNeumann (Order.succ x.rank)
• 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.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.CC'₁.congr_simp 📋 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) (a✝ a✝¹ : ↑(Profinite.NobelingProof.C' C ho)) : a✝ = a✝¹ → Profinite.NobelingProof.CC'₁ C hsC ho a✝ = Profinite.NobelingProof.CC'₁ C hsC ho a✝¹
• 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.CC'₁.eq_1 📋 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) (g : ↑(Profinite.NobelingProof.C' C ho)) : Profinite.NobelingProof.CC'₁ C hsC ho g = ⟨Profinite.NobelingProof.SwapTrue o ↑g, ⋯⟩
• 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.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.GoodProducts.chain'_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.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.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}} (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.Linear_CC'.congr_simp 📋 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 = Profinite.NobelingProof.Linear_CC' C hsC 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.Linear_CC'₁.eq_1 📋 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 = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.CC'₁ C hsC ho, continuous_toFun := ⋯ }
• 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.Linear_CC'.eq_1 📋 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 = Profinite.NobelingProof.Linear_CC'₁ C hsC ho - Profinite.NobelingProof.Linear_CC'₀ C ho
• 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.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 (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 6ff4759 serving mathlib revision 519f454