Theorems · Theorem · logic and foundations
Ordinal.IsFundamentalSeq.comp_isNormal
∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : Ordinal.{u_1} → Ordinal.{u_1}} (hg : Order.IsNormal g),
Ordinal.IsFundamentalSeq f → Order.IsSuccLimit o → Ordinal.IsFundamentalSeq fun i => ⟨g ↑(f i), ⋯⟩If f is a fundamental sequence for a limit ordinal o and g is normal, then g ∘ f is a
fundamental sequence for g o.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.Elemstatement and proof · cited by 7,166
- Set.rangeproof · cited by 4,705
- LE.le.transproof · cited by 3,151
- Cardinalproof · cited by 2,598
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- Ordinalstatement and proof · cited by 1,688
- Set.Iiostatement and proof · cited by 1,166
- Cardinal.ordproof · cited by 266
- Order.IsSuccLimitstatement and proof · cited by 255
- Order.IsNormalstatement and proof · cited by 118
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.