Loogle!

Result

Found 212 declarations mentioning Order.IsSuccLimit. Of these, only the first 200 are shown.

• Order.IsSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] (a : α) : Prop
• Order.IsSuccLimit.isSuccPrelimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {a : α} (self : Order.IsSuccLimit a) : Order.IsSuccPrelimit a
• Order.IsSuccLimit.nonempty_Iio 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] (h : Order.IsSuccLimit a) : (Set.Iio a).Nonempty
• IsMin.not_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] (h : IsMin a) : ¬Order.IsSuccLimit a
• Order.IsSuccLimit.not_isMin 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {a : α} (self : Order.IsSuccLimit a) : ¬IsMin a
• Order.IsSuccLimit.withBotCoe 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : α} : Order.IsSuccLimit x → Order.IsSuccLimit ↑x
• Order.IsSuccLimit.withTopCoe 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : α} : Order.IsSuccLimit x → Order.IsSuccLimit ↑x
• WithBot.isSuccLimit_coe_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : α} : Order.IsSuccLimit ↑x ↔ Order.IsSuccLimit x
• WithTop.isSuccLimit_coe_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : α} : Order.IsSuccLimit ↑x ↔ Order.IsSuccLimit x
• Order.IsSuccPrelimit.isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] : Order.IsSuccPrelimit a → Order.IsSuccLimit a
• Order.isSuccPrelimit_iff_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] : Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a
• Order.not_isSuccLimit_bot 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] [OrderBot α] : ¬Order.IsSuccLimit ⊥
• Order.not_isSuccLimit_of_noMax 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] : ¬Order.IsSuccLimit a
• Order.not_isSuccLimit_succ 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : ¬Order.IsSuccLimit (Order.succ a)
• WithTop.isSuccLimit_top 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] [Nonempty α] [NoMaxOrder α] : Order.IsSuccLimit ⊤
• Order.IsSuccLimit.isMax 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : Order.IsSuccLimit (Order.succ a)) : IsMax a
• Order.IsSuccLimit.mk 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {a : α} (not_isMin : ¬IsMin a) (isSuccPrelimit : Order.IsSuccPrelimit a) : Order.IsSuccLimit a
• Order.IsSuccPrelimit.isSuccLimit_of_not_isMin 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] (h : Order.IsSuccPrelimit a) (ha : ¬IsMin a) : Order.IsSuccLimit a
• Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] (h : ¬IsMin a) : Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a
• Order.not_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] : ¬Order.IsSuccLimit a
• Order.not_isSuccLimit_of_isSuccArchimedean 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] : ¬Order.IsSuccLimit a
• Order.isSuccLimit_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] (a : α) : Order.IsSuccLimit a ↔ ¬IsMin a ∧ Order.IsSuccPrelimit a
• Order.not_isSuccLimit_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) : ¬Order.IsSuccLimit (Order.succ a)
• Order.not_isSuccLimit_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] : ¬Order.IsSuccLimit a ↔ IsMin a ∨ ¬Order.IsSuccPrelimit a
• Order.IsSuccLimit.ne_bot 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [OrderBot α] (h : Order.IsSuccLimit a) : a ≠ ⊥
• Order.IsSuccLimit.ne_zero 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : Order.IsSuccLimit a) : a ≠ 0
• Order.IsSuccLimit.succ_ne 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccLimit a) (b : α) : Order.succ b ≠ a
• Order.IsSuccLimit.bot_lt 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [OrderBot α] (h : Order.IsSuccLimit a) : ⊥ < a
• WithBot.isSuccLimit_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : WithBot α} : Order.IsSuccLimit x ↔ ∃ y, x = ↑y ∧ Order.IsSuccLimit y
• Order.IsSuccLimit.pos 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : Order.IsSuccLimit a) : 0 < a
• WithTop.isSuccLimit_iff_of_isSuccArchimedean 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_2} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] [Nonempty α] {a : WithTop α} : Order.IsSuccLimit a ↔ a = ⊤
• Order.IsPredLimit.dual 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] : Order.IsPredLimit a → Order.IsSuccLimit (OrderDual.toDual a)
• Order.IsSuccLimit.dual 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] : Order.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)
• Order.isPredLimit_toDual_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] : Order.IsPredLimit (OrderDual.toDual a) ↔ Order.IsSuccLimit a
• Order.isSuccLimit_toDual_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [Preorder α] : Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a
• Order.isSuccLimit_iff_of_orderBot 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [PartialOrder α] [OrderBot α] : Order.IsSuccLimit a ↔ a ≠ ⊥ ∧ Order.IsSuccPrelimit a
• Order.IsSuccLimit.succ_lt 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) (ha : a < b) : Order.succ a < b
• Order.isMin_or_mem_range_succ_or_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) : IsMin a ∨ a ∈ Set.range Order.succ ∨ Order.IsSuccLimit a
• WithBot.isSuccPrelimit_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {x : WithBot α} : Order.IsSuccPrelimit x ↔ x = ⊥ ∨ ∃ y, x = ↑y ∧ Order.IsSuccLimit y
• Order.IsSuccLimit.succ_lt_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) : Order.succ a < b ↔ a < b
• WithTop.isSuccLimit_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] [Nonempty α] [NoMaxOrder α] {x : WithTop α} : Order.IsSuccLimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ Order.IsSuccLimit y
• Order.IsSuccLimit.subtypeVal 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) {a : ↑s} (ha : Order.IsSuccLimit a) : Order.IsSuccLimit ↑a
• Order.IsSuccLimit.isLUB_Iio 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] (ha : Order.IsSuccLimit a) : IsLUB (Set.Iio a) a
• IsLUB.isSuccLimit_of_notMem 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) : Order.IsSuccLimit a
• IsLUB.mem_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : ¬Order.IsSuccLimit a) : a ∈ s
• Order.isSuccLimitRecOn 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} (b : α) {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) : motive b
• Order.isSuccLimitRecOn_of_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : Order.IsSuccLimit b) : Order.isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb
• SuccOrder.limitRecOn 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} (b : α) {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) : motive b
• Order.IsSuccLimit.le_iff_forall_le 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a b : α} [LinearOrder α] (h : Order.IsSuccLimit a) : a ≤ b ↔ ∀ c < a, c ≤ b
• Order.IsSuccLimit.lt_iff_exists_lt 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a b : α} [LinearOrder α] (h : Order.IsSuccLimit b) : a < b ↔ ∃ c < b, a < c
• Order.IsSuccLimit.le_succ_iff 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) : b ≤ Order.succ a ↔ b ≤ a
• SuccOrder.limitRecOn_isMin 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : IsMin b) : SuccOrder.limitRecOn b isMin succ isSuccLimit = isMin b hb
• SuccOrder.limitRecOn_of_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : Order.IsSuccLimit b) : SuccOrder.limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x x_1 => SuccOrder.limitRecOn x isMin succ isSuccLimit
• Order.isSuccLimitRecOn_of_isMin 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [LinearOrder α] [SuccOrder α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : IsMin b) : Order.isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb
• Order.isSuccLimitRecOn_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [LinearOrder α] [SuccOrder α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) (hb : ¬IsMax b) : Order.isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb
• Order.isSuccLimitRecOn_succ 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {motive : α → Sort u_2} [LinearOrder α] [SuccOrder α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → motive a) [NoMaxOrder α] (b : α) : Order.isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯
• SuccOrder.limitRecOn_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {b : α} {motive : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) (hb : ¬IsMax b) : SuccOrder.limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (SuccOrder.limitRecOn b isMin succ isSuccLimit)
• SuccOrder.limitRecOn_succ 📋 Mathlib.Order.SuccPred.Limit
  {α : Type u_1} {motive : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (isMin : (a : α) → IsMin a → motive a) (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)) (isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) [NoMaxOrder α] (b : α) : SuccOrder.limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯ (SuccOrder.limitRecOn b isMin succ isSuccLimit)
• Order.not_isSuccLimit_add_one 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_1} [PartialOrder α] (a : α) [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] : ¬Order.IsSuccLimit (a + 1)
• Order.not_isSuccLimit_natCast 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_1} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] (n : ℕ) : ¬Order.IsSuccLimit ↑n
• Order.IsSuccLimit.add_one_lt 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_1} {x y : α} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] (hx : Order.IsSuccLimit x) (hy : y < x) : y + 1 < x
• Order.IsSuccLimit.natCast_lt 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_1} {x : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] (hx : Order.IsSuccLimit x) (n : ℕ) : ↑n < x
• Order.IsSuccLimit.add_natCast_lt 📋 Mathlib.Algebra.Order.SuccPred
  {α : Type u_1} {x y : α} [PartialOrder α] [AddMonoidWithOne α] [SuccAddOrder α] (hx : Order.IsSuccLimit x) (hy : y < x) (n : ℕ) : y + ↑n < x
• IsLUB.mem_of_nonempty_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} {x : α} (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬Order.IsSuccLimit x) : x ∈ s
• IsLUB.exists_of_nonempty_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α} (hf : IsLUB (Set.range f) x) (hx : ¬Order.IsSuccLimit x) : ∃ i, f i = x
• Order.IsSuccLimit.sSup_Iio 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {x : α} (h : Order.IsSuccLimit x) : sSup (Set.Iio x) = x
• csSup_mem_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrder α] {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬Order.IsSuccLimit (sSup s)) : sSup s ∈ s
• exists_eq_ciSup_of_not_isSuccLimit 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {ι : Sort u_1} {α : Type u_2} [ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} (hbdd : BddAbove (Set.range f)) (hf : ¬Order.IsSuccLimit (⨆ i, f i)) : ∃ i, f i = ⨆ i, f i
• Order.IsSuccLimit.iSup_Iio 📋 Mathlib.Order.SuccPred.CompleteLinearOrder
  {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] {x : α} (h : Order.IsSuccLimit x) : ⨆ a, ↑a = x
• Cardinal.IsStrongLimit.isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Order
  {c : Cardinal.{u_1}} (hc : c.IsStrongLimit) : Order.IsSuccLimit c
• Cardinal.not_isSuccLimit_zero 📋 Mathlib.SetTheory.Cardinal.Order
  : ¬Order.IsSuccLimit 0
• Cardinal.ne_zero_of_isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Order
  {c : ℕ} (h : Order.IsSuccLimit c) : c ≠ 0
• Cardinal.isSuccLimit_iff 📋 Mathlib.SetTheory.Cardinal.Order
  {c : Cardinal.{u_1}} : Order.IsSuccLimit c ↔ c ≠ 0 ∧ Order.IsSuccPrelimit c
• Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Order
  {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (Set.range f)) {c : Cardinal.{v}} (hc : ¬Order.IsSuccLimit c) (h : ⨆ i, f i = c) : ∃ i, f i = c
• Cardinal.isSuccLimit_aleph0 📋 Mathlib.SetTheory.Cardinal.Basic
  : Order.IsSuccLimit Cardinal.aleph0
• Cardinal.not_isSuccLimit_natCast 📋 Mathlib.SetTheory.Cardinal.Basic
  (n : ℕ) : ¬Order.IsSuccLimit ↑n
• Cardinal.aleph0_le_of_isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Basic
  {c : Cardinal.{u_1}} (h : Order.IsSuccLimit c) : Cardinal.aleph0 ≤ c
• Cardinal.not_isSuccLimit_of_lt_aleph0 📋 Mathlib.SetTheory.Cardinal.Basic
  {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) : ¬Order.IsSuccLimit c
• InitialSeg.map_isSuccLimit 📋 Mathlib.Order.SuccPred.InitialSeg
  {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : α ≤i β) : Order.IsSuccLimit a → Order.IsSuccLimit (f a)
• InitialSeg.isSuccLimit_apply_iff 📋 Mathlib.Order.SuccPred.InitialSeg
  {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : α ≤i β) : Order.IsSuccLimit (f a) ↔ Order.IsSuccLimit a
• PrincipalSeg.map_isSuccLimit 📋 Mathlib.Order.SuccPred.InitialSeg
  {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : α <i β) : Order.IsSuccLimit a → Order.IsSuccLimit (f.toRelEmbedding a)
• PrincipalSeg.isSuccLimit_apply_iff 📋 Mathlib.Order.SuccPred.InitialSeg
  {α : Type u_1} {β : Type u_2} {a : α} [PartialOrder α] [PartialOrder β] (f : α <i β) : Order.IsSuccLimit (f.toRelEmbedding a) ↔ Order.IsSuccLimit a
• Order.IsNormal.map_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : Order.IsNormal f) (ha : Order.IsSuccLimit a) : Order.IsSuccLimit (f a)
• Order.IsNormal.isLUB_image_Iio_of_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Order.IsNormal f) {a : α} (ha : Order.IsSuccLimit a) : IsLUB (f '' Set.Iio a) (f a)
• Order.IsNormal.le_iff_forall_le 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : Order.IsNormal f) (ha : Order.IsSuccLimit a) {b : β} : f a ≤ b ↔ ∀ a' < a, f a' ≤ b
• Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (self : Order.IsNormal f) {a : α} (ha : Order.IsSuccLimit a) : f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
• Order.IsNormal.lt_iff_exists_lt 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : Order.IsNormal f) (ha : Order.IsSuccLimit a) {b : β} : b < f a ↔ ∃ a' < a, b < f a'
• Order.IsNormal.mk 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (strictMono : StrictMono f) (mem_lowerBounds_upperBounds_of_isSuccLimit : ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))) : Order.IsNormal f
• Order.isNormal_iff 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} : Order.IsNormal f ↔ StrictMono f ∧ ∀ (o : α), Order.IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a
• Order.isNormal_iff' 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) : Order.IsNormal f ↔ StrictMono f ∧ ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
• Order.IsNormal.apply_of_isSuccLimit 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [ConditionallyCompleteLinearOrderBot α] [ConditionallyCompleteLinearOrder β] (hf : Order.IsNormal f) (ha : Order.IsSuccLimit a) : f a = ⨆ b, f ↑b
• Order.IsNormal.of_succ_lt 📋 Mathlib.Order.IsNormal
  {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [WellFoundedLT α] [SuccOrder α] [LinearOrder β] (hs : ∀ (a : α), f a < f (Order.succ a)) (hl : ∀ {a : α}, Order.IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)) : Order.IsNormal f
• Ordinal.isSuccLimit_omega0 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  : Order.IsSuccLimit Ordinal.omega0
• Ordinal.not_isSuccLimit_zero 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  : ¬Order.IsSuccLimit 0
• Order.IsSuccLimit.ordinalPred_eq 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} (ho : Order.IsSuccLimit o) : o.pred = o
• Cardinal.isSuccLimit_ord 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) : Order.IsSuccLimit c.ord
• Ordinal.isSuccLimit_lift 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{v}} : Order.IsSuccLimit (Ordinal.lift.{u, v} o) ↔ Order.IsSuccLimit o
• Ordinal.omega0_le_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) : Ordinal.omega0 ≤ o
• Ordinal.one_lt_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) : 1 < o
• Ordinal.isSuccLimit_add 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} : Order.IsSuccLimit b → Order.IsSuccLimit (a + b)
• Ordinal.natCast_lt_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} (h : Order.IsSuccLimit o) (n : ℕ) : ↑n < o
• Ordinal.isSuccLimit_iff 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {o : Ordinal.{u_4}} : Order.IsSuccLimit o ↔ o ≠ 0 ∧ Order.IsSuccPrelimit 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.isSuccPrelimit_mul_left 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (ha : Order.IsSuccLimit a) : Order.IsSuccPrelimit (a * b)
• Ordinal.isSuccPrelimit_mul_right 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) : Order.IsSuccPrelimit (a * b)
• Ordinal.isSuccLimit_add_iff_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (h : Order.IsSuccLimit a) : Order.IsSuccLimit (a + b) ↔ Order.IsSuccPrelimit b
• Ordinal.isSuccLimit_sub 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (ha : Order.IsSuccPrelimit a) (h : b < a) : Order.IsSuccLimit (a - b)
• 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.isSuccLimit_add_iff 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} : Order.IsSuccLimit (a + b) ↔ Order.IsSuccLimit b ∨ b = 0 ∧ Order.IsSuccLimit a
• Ordinal.isSuccLimit_mul_left 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (l : Order.IsSuccLimit a) (b0 : 0 < b) : Order.IsSuccLimit (a * b)
• Ordinal.isSuccLimit_mul_right 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b : Ordinal.{u_4}} (a0 : 0 < a) (l : Order.IsSuccLimit b) : Order.IsSuccLimit (a * b)
• Ordinal.limitRecOn 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {motive : Ordinal.{u_5} → Sort u_4} (o : Ordinal.{u_5}) (zero : motive 0) (add_one : (o : Ordinal.{u_5}) → motive o → motive (o + 1)) (limit : (o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) : motive o
• Ordinal.add_le_iff_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (hb : Order.IsSuccLimit b) : a + b ≤ c ↔ ∀ d < b, a + d ≤ c
• Ordinal.lt_add_iff_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (hc : Order.IsSuccLimit c) : a < b + c ↔ ∃ d < c, a < b + d
• Ordinal.add_mul_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (ba : b + a = a) (l : Order.IsSuccLimit c) : (a + b) * c = a * c
• Ordinal.mul_le_iff_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c
• 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 (o + 1)) (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.lt_mul_iff_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a b c : Ordinal.{u_4}} (h : Order.IsSuccLimit c) : a < b * c ↔ ∃ c' < c, a < b * c'
• 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 (o + 1)) (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.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 (o + 1)) (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.limitRecOn_add_one 📋 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 (o + 1)) (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o) : Ordinal.limitRecOn (o + 1) H₁ H₂ H₃ = H₂ o (Ordinal.limitRecOn o H₁ H₂ H₃)
• Ordinal.IsNormal.blsub_eq 📋 Mathlib.SetTheory.Ordinal.Family
  {f : Ordinal.{u} → Ordinal.{max u v}} (H : Order.IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) : (o.blsub fun x x_1 => f x) = f o
• Ordinal.IsNormal.bsup_eq 📋 Mathlib.SetTheory.Ordinal.Family
  {f : Ordinal.{u} → Ordinal.{max u v}} (H : Order.IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) : (o.bsup fun x x_1 => f x) = f o
• 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_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.isSuccLimit_opow_left 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b : Ordinal.{u_1}} (l : Order.IsSuccLimit a) (hb : b ≠ 0) : Order.IsSuccLimit (a ^ b)
• Ordinal.isSuccLimit_opow 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b : Ordinal.{u_1}} (a1 : 1 < a) : Order.IsSuccLimit b → Order.IsSuccLimit (a ^ b)
• Ordinal.opow_le_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b c : Ordinal.{u_1}} (a0 : a ≠ 0) (h : Order.IsSuccLimit b) : a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c
• Ordinal.lt_opow_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b c : Ordinal.{u_1}} (b0 : b ≠ 0) (h : Order.IsSuccLimit c) : a < b ^ c ↔ ∃ c' < c, a < b ^ c'
• Ordinal.opow_limit 📋 Mathlib.SetTheory.Ordinal.Exponential
  {a b : Ordinal.{u_1}} (ha : a ≠ 0) (hb : Order.IsSuccLimit b) : a ^ b = ⨆ x, a ^ ↑x
• Ordinal.derivFamily_limit 📋 Mathlib.SetTheory.Ordinal.FixedPoint
  {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}) {o : Ordinal.{u_2}} : Order.IsSuccLimit o → Ordinal.derivFamily f o = ⨆ b, Ordinal.derivFamily f ↑b
• Ordinal.deriv_limit 📋 Mathlib.SetTheory.Ordinal.FixedPoint
  (f : Ordinal.{u_1} → Ordinal.{u_1}) {o : Ordinal.{u_1}} : Order.IsSuccLimit o → Ordinal.deriv f o = ⨆ a, Ordinal.deriv f ↑a
• Ordinal.isSuccLimit_of_isPrincipal_add 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} (ho₁ : 1 < o) (ho : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o) : Order.IsSuccLimit o
• Ordinal.isSuccLimit_of_principal_add 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} (ho₁ : 1 < o) (ho : Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o) : Order.IsSuccLimit o
• Ordinal.op_eq_self_of_isPrincipal 📋 Mathlib.SetTheory.Ordinal.Principal
  {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (H : Order.IsNormal (op a)) (ho : Ordinal.IsPrincipal op o) (ho' : Order.IsSuccLimit o) : op a o = o
• Ordinal.op_eq_self_of_principal 📋 Mathlib.SetTheory.Ordinal.Principal
  {a o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}} (hao : a < o) (H : Order.IsNormal (op a)) (ho : Ordinal.IsPrincipal op o) (ho' : Order.IsSuccLimit o) : op a o = o
• Ordinal.isSuccLimit_of_isPrincipal_mul 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o) : Order.IsSuccLimit o
• Ordinal.isSuccLimit_of_principal_mul 📋 Mathlib.SetTheory.Ordinal.Principal
  {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o) : Order.IsSuccLimit o
• Cardinal.isStrongLimit_preBeth 📋 Mathlib.SetTheory.Cardinal.Aleph
  {o : Ordinal.{u_1}} : (Cardinal.preBeth o).IsStrongLimit ↔ Order.IsSuccLimit o
• Cardinal.isSuccLimit_omega 📋 Mathlib.SetTheory.Cardinal.Aleph
  (o : Ordinal.{u_1}) : Order.IsSuccLimit (Ordinal.omega o)
• Cardinal.beth_limit 📋 Mathlib.SetTheory.Cardinal.Aleph
  {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) : Cardinal.beth o = ⨆ a, Cardinal.beth ↑a
• Cardinal.aleph_limit 📋 Mathlib.SetTheory.Cardinal.Aleph
  {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) : Cardinal.aleph o = ⨆ a, Cardinal.aleph ↑a
• Ordinal.aleph0_le_cof 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {o : Ordinal.{u_1}} : Cardinal.aleph0 ≤ o.cof ↔ Order.IsSuccLimit o
• Ordinal.cof_eq_of_isNormal 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) : (f a).cof = a.cof
• Ordinal.cof_map_of_isNormal 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : Order.IsNormal f) {a : Ordinal.{u_1}} (ha : Order.IsSuccLimit a) : (f a).cof = a.cof
• Ordinal.one_lt_cof_iff 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {o : Ordinal.{u_1}} : 1 < o.cof ↔ Order.IsSuccLimit o
• Ordinal.cof_omega 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) : (Ordinal.omega o).cof = o.cof
• 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_eq_aleph0_of_isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
  {o : Ordinal.{u_1}} (ho : Order.IsSuccLimit o) (ho' : o < Ordinal.omega 1) : o.cof = Cardinal.aleph0
• Ordinal.IsFundamentalSequence.of_isNormal 📋 Mathlib.SetTheory.Ordinal.FundamentalSequence
  {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) {a o : Ordinal.{u}} (ha : Order.IsSuccLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun b hb => f (g b hb)
• Ordinal.IsFundamentalSeq.comp_isNormal 📋 Mathlib.SetTheory.Ordinal.FundamentalSequence
  {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : Ordinal.{u_1} → Ordinal.{u_1}} (hg : Order.IsNormal g) (hf : Ordinal.IsFundamentalSeq f) (ho : Order.IsSuccLimit o) : Ordinal.IsFundamentalSeq fun i => ⟨g ↑(f i), ⋯⟩
• Cardinal.IsInaccessible.isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Regular
  {c : Cardinal.{u_1}} (h : c.IsInaccessible) : Order.IsSuccLimit c
• Cardinal.IsSingular.isSuccLimit 📋 Mathlib.SetTheory.Cardinal.Regular
  {c : Cardinal.{u_1}} (hc : c.IsSingular) : Order.IsSuccLimit c
• Cardinal.isRegular_cof 📋 Mathlib.SetTheory.Cardinal.Regular
  {o : Ordinal.{u_1}} (h : Order.IsSuccLimit o) : o.cof.IsRegular
• Cardinal.IsSingular.isSuccLimit_of_aleph 📋 Mathlib.SetTheory.Cardinal.Regular
  {o : Ordinal.{u_1}} (hc : (Cardinal.aleph o).IsSingular) : Order.IsSuccLimit o
• Cardinal.isSingular_aleph_iff 📋 Mathlib.SetTheory.Cardinal.Regular
  {o : Ordinal.{u_1}} : (Cardinal.aleph o).IsSingular ↔ Order.IsSuccLimit o ∧ o.cof < Cardinal.aleph o
• transfiniteIterate_limit 📋 Mathlib.Order.TransfiniteIteration
  {I : Type u} [SupSet I] (φ : I → I) {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] (i₀ : I) (j : J) (hj : Order.IsSuccLimit j) : transfiniteIterate φ j i₀ = ⨆ x, transfiniteIterate φ (↑x) i₀
• Set.Ici.isSuccLimit_coe 📋 Mathlib.Order.Interval.Set.Limit
  {J : Type u} [LinearOrder J] {j : J} (m : ↑(Set.Ici j)) (hm : Order.IsSuccLimit m) : Order.IsSuccLimit ↑m
• CategoryTheory.Functor.isColimitOfIsWellOrderContinuous' 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [PartialOrder J] (F : CategoryTheory.Functor J C) [F.IsWellOrderContinuous] {α : Type u_1} [PartialOrder α] (f : α <i J) (hα : Order.IsSuccLimit f.top) : CategoryTheory.Limits.IsColimit (f.cocone F)
• CategoryTheory.Functor.isColimitOfIsWellOrderContinuous 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [PartialOrder J] (F : CategoryTheory.Functor J C) [F.IsWellOrderContinuous] (m : J) (hm : Order.IsSuccLimit m) : CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F)
• CategoryTheory.Functor.IsWellOrderContinuous.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [PartialOrder J] {F : CategoryTheory.Functor J C} (nonempty_isColimit : ∀ (m : J), Order.IsSuccLimit m → Nonempty (CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F))) : F.IsWellOrderContinuous
• CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : Type w} {inst✝¹ : PartialOrder J} {F : CategoryTheory.Functor J C} [self : F.IsWellOrderContinuous] (m : J) (hm : Order.IsSuccLimit m) : Nonempty (CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F))
• CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
  {J : Type w} [LinearOrder J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : Order.IsSuccLimit j) : CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C
• CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
  {J : Type w} {inst✝ : LinearOrder J} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : Order.IsSuccLimit j) : CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C
• CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit' 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
  {J : Type w} [LinearOrder J] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasIterationOfShape J C] {α : Type u_1} [PartialOrder α] (h : α <i J) (hα : Order.IsSuccLimit h.top) : CategoryTheory.Limits.HasColimitsOfShape α C
• CategoryTheory.Limits.HasIterationOfShape.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
  {J : Type w} [LinearOrder J] {C : Type u} [CategoryTheory.Category.{v, u} C] (hasColimitsOfShape_of_isSuccLimit : ∀ (j : J), Order.IsSuccLimit j → CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C := by infer_instance) (hasColimitsOfShape : CategoryTheory.Limits.HasColimitsOfShape J C := by infer_instance) : CategoryTheory.Limits.HasIterationOfShape J C
• CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {J : Type w} [LinearOrder J] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G] (j : J) (hj : Order.IsSuccLimit j) : CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G
• CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
  {C : Type u} {D : Type u'} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Category.{v', u'} D} {J : Type w} {inst✝² : LinearOrder J} {G : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G] (j : J) (hj : Order.IsSuccLimit j) : CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G
• CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.mk 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {J : Type w} [LinearOrder J] {G : CategoryTheory.Functor C D} (preservesColimitsOfShape : ∀ (j : J), Order.IsSuccLimit j → CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G := by infer_instance) : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G
• CategoryTheory.SmallObject.SuccStruct.arrowι 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [CategoryTheory.Limits.HasIterationOfShape J C] {i : J} (F : CategoryTheory.Functor (↑(Set.Iio i)) C) (hi : Order.IsSuccLimit i) (k : J) (hk : k < i) : CategoryTheory.Arrow C
• CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (self : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i) : CategoryTheory.SmallObject.SuccStruct.arrowMap self.F k i ⋯ hij = CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT self.F hij) hi k hk
• CategoryTheory.SmallObject.SuccStruct.Iteration.isColimit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : CategoryTheory.Limits.IsColimit (CategoryTheory.SmallObject.coconeOfLE iter.F hij)
• CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : iter.F.obj ⟨i, hij⟩ = CategoryTheory.Limits.colimit (CategoryTheory.SmallObject.restrictionLT iter.F hij)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mk 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀) (arrowSucc_eq : ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)) (arrowMap_limit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i), CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij = CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk) : Φ.Iteration j
• CategoryTheory.SmallObject.SuccStruct.arrowι_def 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [CategoryTheory.Limits.HasIterationOfShape J C] {i : J} (F : CategoryTheory.Functor (↑(Set.Iio i)) C) (hi : Order.IsSuccLimit i) (k : J) (hk : k < i) : CategoryTheory.SmallObject.SuccStruct.arrowι F hi k hk = CategoryTheory.Arrow.mk (CategoryTheory.Limits.colimit.ι F ⟨k, hk⟩)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : Φ.Iteration j
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : CategoryTheory.Functor (↑(Set.Iic j)) C
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) : (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i₁ i₂ h₁₂ ⋯ = CategoryTheory.Arrow.mk ((iter i₁ ⋯).mapObj (iter i₂ h₂) h₁₂ ⋯ ⋯ h₁₂)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) : CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i j ⋯ ⋯ = CategoryTheory.Arrow.mk (CategoryTheory.Limits.colimit.ι (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter) ⟨i, hi⟩)
• CategoryTheory.Functor.WellOrderInductionData.Extension.limit 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J) (hj : Order.IsSuccLimit j) (e : (i : J) → i < j → d.Extension val₀ i) : d.Extension val₀ j
• CategoryTheory.Functor.WellOrderInductionData.lift 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} (self : F.WellOrderInductionData) (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) : F.obj (Opposite.op j)
• CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (self : d.Extension val₀ j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) self.val = d.lift i hi ⟨fun x => match x with | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) self.val, ⋯⟩
• CategoryTheory.Functor.WellOrderInductionData.map_lift 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} (self : F.WellOrderInductionData) (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (self.lift j hj x) = ↑x (Opposite.op ⟨i, hi⟩)
• CategoryTheory.Functor.WellOrderInductionData.ofExists 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} (h₁ : ∀ (j : J), ¬IsMax j → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) (h₂ : ∀ (j : J), Order.IsSuccLimit j → ∀ (x : ↑(⋯.functor.op.comp F).sections), ∃ y, ∀ (i : J) (hi : i < j), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) y = ↑x (Opposite.op ⟨i, hi⟩)) : F.WellOrderInductionData
• CategoryTheory.Functor.WellOrderInductionData.Extension.mk 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (val : F.obj (Opposite.op j)) (map_zero : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀) (map_succ : ∀ (i : J) (hi : i < j), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = d.succ i ⋯ ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val)) (map_limit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val = d.lift i hi ⟨fun x => match x with | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val, ⋯⟩) : d.Extension val₀ j
• CategoryTheory.Functor.WellOrderInductionData.mk 📋 Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
  {J : Type u} [LinearOrder J] [SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)} (succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))) (map_succ : ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ j hj x) = x) (lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)) (map_lift : ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j), (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift j hj x) = ↑x (Opposite.op ⟨i, hi⟩)) : F.WellOrderInductionData
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) : F.obj j ⟶ X
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) : (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g).obj (Opposite.op j)
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift_f' 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) : (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift hj s).f' = CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) {i : J} (hij : i < j) : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.lift hj s) (CategoryTheory.homOfLE ⋯) = ↑s (Opposite.op ⟨i, hij⟩)
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) (i : J) (hi : i < j) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s) h) = CategoryTheory.CategoryStruct.comp (↑s (Opposite.op ⟨i, hi⟩)).f' h
• CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j) (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections) (i : J) (hi : i < j) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s) = (↑s (Opposite.op ⟨i, hi⟩)).f'
• SSet.Subcomplex.Pairing.RankFunction.iSup_filtration_iio 📋 Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
  {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι] [SuccOrder ι] (m : ι) (hm : Order.IsSuccLimit m) : ⨆ i, f.filtration ↑i = f.filtration m
• SSet.Subcomplex.Pairing.RankFunction.filtration_of_isSuccLimit 📋 Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
  {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι] [SuccOrder ι] (i : ι) (hi : Order.IsSuccLimit i) : f.filtration i = ⨆ j, ⨆ (_ : j < i), f.filtration j
• OrdinalApprox.gfpApprox_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.FixedPointApproximants
  {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (ha : Order.IsSuccLimit a) : OrdinalApprox.gfpApprox f x a = ⨅ b, OrdinalApprox.gfpApprox f x ↑b
• OrdinalApprox.lfpApprox_of_isSuccLimit 📋 Mathlib.SetTheory.Ordinal.FixedPointApproximants
  {α : Type u} [CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}} (ha : Order.IsSuccLimit a) : OrdinalApprox.lfpApprox f x a = ⨆ b, OrdinalApprox.lfpApprox f x ↑b
• ONote.fundamentalSequenceProp_inr 📋 Mathlib.SetTheory.Ordinal.Notation
  (o : ONote) (f : ℕ → ONote) : o.FundamentalSequenceProp (Sum.inr f) ↔ Order.IsSuccLimit o.repr ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a < o.repr, ∃ i, a < (f i).repr
• AccPt.isSuccLimit 📋 Mathlib.Topology.Order.SuccPred
  {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α] {a : α} {s : Set α} (h : AccPt a (Filter.principal s)) : Order.IsSuccLimit a

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 ce5dd8c