Documentation Verification Report

FundamentalSequence

📁 Source: Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

Statistics

Metric	Count
Definitions `IsFundamentalSeq`, `IsFundamentalSequence`	2
Theorems `add_one`, `comp`, `comp_isNormal`, `iSup_add_one_eq`, `iSup_eq`, `id`, `isCofinal_range`, `le_ord_cof`, `ord_cof`, `strictMono`, `zero`, `blsub_eq`, `cof_eq`, `id_of_le_cof`, `lt`, `monotone`, `of_isNormal`, `ord_cof`, `strict_mono`, `succ`, `trans`, `zero`, `isFundamentalSequence`, `exists_fundamental_sequence`, `exists_isFundamentalSeq`	25
Total	27

Ordinal

Definitions

Name	Category	Theorems
`IsFundamentalSeq` 📖	CompData	6 math math: `IsFundamentalSeq.zero`, `IsFundamentalSeq.add_one`, `exists_isFundamentalSeq`, `IsFundamentalSeq.id`, `IsFundamentalSeq.comp`, `IsFundamentalSeq.comp_isNormal`
`IsFundamentalSequence` 📖	MathDef	8 math math: `IsFundamentalSequence.of_isNormal`, `IsNormal.isFundamentalSequence`, `IsFundamentalSequence.trans`, `IsFundamentalSequence.id_of_le_cof`, `exists_fundamental_sequence`, `IsFundamentalSequence.ord_cof`, `IsFundamentalSequence.succ`, `IsFundamentalSequence.zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_fundamental_sequence` 📖	mathematical	—	`IsFundamentalSequence` `Cardinal.ord` `cof`	—	`exists_lsub_cof` `Cardinal.ord_eq` `RelEmbedding.isWellOrder` `LE.le.trans` `RelEmbedding.ordinal_type_le` `le_refl` `Subtype.prop` `RelEmbedding.map_rel_iff'` `enum_lt_enum` `le_antisymm` `blsub_le` `lsub_le_iff` `Eq.le` `typein_lt_type` `bfamilyOfFamily'_typein` `IsWellFounded.wf` `IsWellOrder.toIsWellFounded` `Mathlib.Tactic.Push.not_forall_eq` `WellFounded.min_mem` `lt_of_lt_of_le` `WellFounded.not_lt_min` `IsTrans.trans` `instIsTransOfIsWellOrder` `LE.le.trans_lt` `lt_blsub` `LT.lt.trans_le` `IsFundamentalSequence.ord_cof`
`exists_isFundamentalSeq` 📖	mathematical	`Cardinal.ord` `cof`	`IsFundamentalSeq`	—	`isWellOrder_lt` `Subtype.wellFoundedLT` `wellFoundedLT_toType` `ord_cof_eq` `cof_toType` `le_rfl` `Set.range_comp'` `OrderIso.map_isCofinal_iff` `OrderIso.range_eq` `Set.image_univ` `Subtype.range_coe_subtype`

Ordinal.IsFundamentalSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one` 📖	mathematical	—	`Ordinal.IsFundamentalSeq` `Ordinal` `Ordinal.one` `Ordinal.add` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `lt_add_one` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ordinal.addMonoidWithOne` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `Ordinal.instAddLeftStrictMono`	—	`lt_add_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne` `Ordinal.instAddLeftStrictMono` `Ordinal.cof_add` `Ordinal.cof_one` `Cardinal.ord_one` `instReflLe` `Unique.instSubsingleton` `Set.range_const` `Ordinal.instNoMaxOrder`
`comp` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`Ordinal.IsFundamentalSeq` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`ord_cof` `Ordinal.ord_cof_le` `StrictMono.comp` `strictMono` `Set.range_comp` `IsCofinal.image` `isCofinal_range` `StrictMono.monotone`
`comp_isNormal` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder` `Ordinal.IsFundamentalSeq` `Order.IsSuccLimit` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal.IsFundamentalSeq` `Ordinal` `Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Order.IsNormal.strictMono` `Ordinal.instLinearOrder`	—	`Order.IsNormal.strictMono` `Ordinal.cof_map_of_isNormal` `ord_cof` `le_refl` `StrictMono.comp` `strictMono` `Order.IsNormal.lt_iff_exists_lt` `Set.mem_Iio` `isCofinal_range` `LE.le.trans` `LT.lt.le` `Order.IsNormal.monotone`
`iSup_add_one_eq` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`iSup` `Ordinal` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Ordinal.add` `Set` `Set.instMembership` `Ordinal.one`	—	`le_antisymm` `Ordinal.small_Iio` `Ordinal.instNoMaxOrder` `le_of_forall_lt` `isCofinal_range` `LE.le.trans_lt` `Order.add_one_le_iff` `Ordinal.le_iSup`
`iSup_eq` 📖	mathematical	`Ordinal.IsFundamentalSeq` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one`	`iSup` `Ordinal` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`Ordinal.iSup_Iio_add_one` `strictMono` `ord_cof` `Order.IsSuccLimit.isSuccPrelimit` `Cardinal.isSuccLimit_ord` `Ordinal.aleph0_le_cof_iff` `Cardinal.ord_lt_ord` `Cardinal.ord_one` `iSup_add_one_eq`
`id` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Cardinal.ord` `Ordinal.cof`	`Ordinal.IsFundamentalSeq` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`strictMono_id` `Set.range_id`
`isCofinal_range` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`IsCofinal` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Preorder.toLE` `Set` `Set.instMembership` `Set.range`	—	—
`le_ord_cof` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Cardinal.ord` `Ordinal.cof`	—	—
`ord_cof` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`Cardinal.ord` `Ordinal.cof`	—	`LE.le.antisymm'` `le_ord_cof` `iSup_add_one_eq` `Ordinal.cof_iSup_Iio_add_one` `strictMono` `Ordinal.ord_cof_le`
`strictMono` 📖	mathematical	`Ordinal.IsFundamentalSeq`	`StrictMono` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Subtype.preorder` `Set` `Set.instMembership`	—	—
`zero` 📖	mathematical	—	`Ordinal.IsFundamentalSeq` `Ordinal` `Ordinal.zero`	—	`Ordinal.cof_zero` `Cardinal.ord_zero` `instReflLe` `IsEmpty.instSubsingleton` `Ordinal.instIsEmptyIioZero` `Set.range_eq_empty` `isCofinal_empty_iff`

Ordinal.IsFundamentalSequence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`blsub_eq` 📖	mathematical	`Ordinal.IsFundamentalSequence`	`Ordinal.blsub`	—	—
`cof_eq` 📖	mathematical	`Ordinal.IsFundamentalSequence`	`Cardinal.ord` `Ordinal.cof`	—	`LE.le.antisymm'` `LE.le.trans` `Cardinal.ord_le_ord` `Ordinal.cof_blsub_le` `Cardinal.ord_card_le`
`id_of_le_cof` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Cardinal.ord` `Ordinal.cof`	`Ordinal.IsFundamentalSequence`	—	`Ordinal.blsub_id`
`lt` 📖	mathematical	`Ordinal.IsFundamentalSequence` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`Ordinal.lt_blsub` `blsub_eq`
`monotone` 📖	mathematical	`Ordinal.IsFundamentalSequence` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Preorder.toLE`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`lt_or_eq_of_le` `LT.lt.le` `le_refl`
`of_isNormal` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder` `Order.IsSuccLimit` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.IsFundamentalSequence`	`Ordinal.IsFundamentalSequence`	—	`Ordinal.exists_lsub_cof` `cof_eq` `Cardinal.ord_le_ord` `Ordinal.lt_lsub` `Ordinal.lt_blsub_iff` `Ordinal.IsNormal.blsub_eq` `LE.le.antisymm` `Ordinal.lsub_le` `lt_of_le_of_lt` `csInf_le'` `le_of_forall_lt` `Order.IsNormal.strictMono` `Ordinal.lt_lsub_iff` `LE.le.trans_lt` `le_csInf_iff''` `StrictMono.le_iff_le` `LE.le.trans` `Ordinal.cof_lsub_le` `Ordinal.blsub_comp` `StrictMono.monotone`
`ord_cof` 📖	mathematical	`Ordinal.IsFundamentalSequence`	`Ordinal.IsFundamentalSequence` `Cardinal.ord` `Ordinal.cof` `LT.lt.trans_le` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`cof_eq` `LT.lt.trans_le`
`strict_mono` 📖	mathematical	`Ordinal.IsFundamentalSequence` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	—
`succ` 📖	mathematical	—	`Ordinal.IsFundamentalSequence` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `Ordinal.one`	—	`Ordinal.cof_succ` `Cardinal.ord_one` `le_refl` `LT.lt.false` `Ordinal.lt_one_iff_zero` `Ordinal.blsub_const` `Ordinal.one_ne_zero`
`trans` 📖	mathematical	`Ordinal.IsFundamentalSequence`	`Ordinal.IsFundamentalSequence`	—	`cof_eq` `LE.le.trans` `Ordinal.ord_cof_le` `Ordinal.blsub_comp` `monotone`
`zero` 📖	mathematical	—	`Ordinal.IsFundamentalSequence` `Ordinal` `Ordinal.zero`	—	`Ordinal.cof_zero` `Cardinal.ord_zero` `le_refl` `not_lt_zero` `Ordinal.canonicallyOrderedAdd` `Ordinal.blsub_zero`

Ordinal.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFundamentalSequence` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder` `Order.IsSuccLimit` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.IsFundamentalSequence`	`Ordinal.IsFundamentalSequence`	—	`Ordinal.IsFundamentalSequence.of_isNormal`

---

← Back to Index