Documentation Verification Report

OrderIsoNat

📁 Source: Mathlib/Order/OrderIsoNat.lean

Statistics

Metric	Count
Definitions `orderIsoOfNat`, `orderEmbeddingOfSet`, `natGT`, `natLT`, `monotonicSequenceLimit`, `monotonicSequenceLimitIndex`	6
Theorems `orderIsoOfNat_apply`, `coe_orderEmbeddingOfSet`, `exists_subseq_of_forall_mem_union`, `orderEmbeddingOfSet_apply`, `orderEmbeddingOfSet_range`, `acc_iff_isEmpty_subtype_mem_range`, `coe_natGT`, `coe_natLT`, `not_acc`, `not_wellFounded`, `wellFounded_iff_isEmpty`, `ciSup_eq_monotonicSequenceLimit`, `iSup_eq_monotonicSequenceLimit`, `monotone_chain_condition`, `monotone_chain_condition'`, `exists_covBy_seq_of_wellFoundedLT_wellFoundedGT`, `exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le`, `exists_increasing_or_nonincreasing_subseq`, `exists_increasing_or_nonincreasing_subseq'`, `le_monotonicSequenceLimit`, `not_strictAnti_of_wellFoundedLT`, `not_strictMono_of_wellFoundedGT`, `wellFoundedGT_iff_monotone_chain_condition`, `wellFoundedGT_iff_monotone_chain_condition'`	24
Total	30

Nat

Definitions

Name	Category	Theorems
`orderEmbeddingOfSet` 📖	CompOp	3 math math: `orderEmbeddingOfSet_apply`, `coe_orderEmbeddingOfSet`, `orderEmbeddingOfSet_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_orderEmbeddingOfSet` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `orderEmbeddingOfSet` `Set.Elem` `Set` `Set.instMembership` `Subtype.ofNat`	—	—
`exists_subseq_of_forall_mem_union` 📖	mathematical	`Set` `Set.instMembership` `Set.instUnion`	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`Set.eq_univ_of_forall` `Set.mem_preimage` `instInfiniteNat`
`orderEmbeddingOfSet_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `orderEmbeddingOfSet` `Set` `Set.instMembership` `Subtype.ofNat`	—	—
`orderEmbeddingOfSet_range` 📖	mathematical	—	`Set.range` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `orderEmbeddingOfSet`	—	`Subtype.coe_comp_ofNat_range`

Nat.Subtype

Definitions

Name	Category	Theorems
`orderIsoOfNat` 📖	CompOp	3 math math: `orderIsoOfNat_apply`, `Nat.nth_apply_eq_orderIsoOfNat`, `Nat.nth_eq_orderIsoOfNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoOfNat_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Set.Elem` `Set` `Set.instMembership` `instFunLikeOrderIso` `orderIsoOfNat` `ofNat`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`

RelEmbedding

Definitions

Name	Category	Theorems
`natGT` 📖	CompOp	1 math math: `coe_natGT`
`natLT` 📖	CompOp	1 math math: `coe_natLT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc_iff_isEmpty_subtype_mem_range` 📖	mathematical	—	`IsEmpty` `RelEmbedding` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `instFunLike`	—	`not_acc_iff_exists_descending_chain` `map_rel_iff` `of_not_not`
`coe_natGT` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `natGT`	—	—
`coe_natLT` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `natLT`	—	—
`not_acc` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	`acc_iff_isEmpty_subtype_mem_range` `not_isEmpty_iff`
`not_wellFounded` 📖	—	—	—	—	`wellFounded_iff_isEmpty` `not_isEmpty_iff`
`wellFounded_iff_isEmpty` 📖	mathematical	—	`IsEmpty` `RelEmbedding`	—	`not_acc` `acc_iff_isEmpty_subtype_mem_range` `instIsEmptySubtype`

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciSup_eq_monotonicSequenceLimit` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `monotonicSequenceLimit`	—	`LE.le.antisymm` `ciSup_le` `le_monotonicSequenceLimit` `le_ciSup`
`iSup_eq_monotonicSequenceLimit` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `OrderHom.instFunLike` `monotonicSequenceLimit`	—	`LE.le.antisymm` `iSup_le` `le_monotonicSequenceLimit` `le_iSup`
`monotone_chain_condition` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `OrderHom.instFunLike`	—	`wellFoundedGT_iff_monotone_chain_condition`
`monotone_chain_condition'` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike`	—	`wellFoundedGT_iff_monotone_chain_condition'`

(root)

Definitions

Name	Category	Theorems
`monotonicSequenceLimit` 📖	CompOp	3 math math: `WellFoundedGT.iSup_eq_monotonicSequenceLimit`, `le_monotonicSequenceLimit`, `WellFoundedGT.ciSup_eq_monotonicSequenceLimit`
`monotonicSequenceLimitIndex` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_covBy_seq_of_wellFoundedLT_wellFoundedGT` 📖	mathematical	—	`IsMin` `Preorder.toLE` `IsMax` `CovBy` `Preorder.toLT`	—	`Set.nonempty_iff_univ_nonempty` `IsWellFounded.wf` `isMin_iff_forall_not_lt` `WellFounded.not_lt_min` `RelEmbedding.not_wellFounded` `instIsStrictOrderGt` `wellFounded_lt` `instWellFoundedLTNat` `WellFounded.min_mem` `exists_covBy_of_wellFoundedLT`
`exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`CovBy` `Preorder.toLT`	—	`le_rfl` `exists_covBy_seq_of_wellFoundedLT_wellFoundedGT` `bot_nonempty` `Subtype.wellFoundedLT` `Subtype.wellFoundedGT` `LE.le.trans` `LT.lt.le`
`exists_increasing_or_nonincreasing_subseq` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`exists_increasing_or_nonincreasing_subseq'` `IsTrans.trans` `lt_of_lt_of_le`
`exists_increasing_or_nonincreasing_subseq'` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	—	`Set.mem_range_self` `Nat.orderEmbeddingOfSet_range` `OrderEmbedding.lt_iff_lt` `Set.Infinite.eq_1` `Set.infinite_coe_iff` `LE.le.trans` `Finset.le_max'` `Set.Finite.mem_toFinset` `instIsStrictOrderLt` `Nat.find_spec`
`le_monotonicSequenceLimit` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `monotonicSequenceLimit`	—	`le_or_gt` `OrderHom.monotone` `Eq.ge` `Nat.sInf_mem` `WellFoundedGT.monotone_chain_condition` `LT.lt.le`
`not_strictAnti_of_wellFoundedLT` 📖	mathematical	—	`StrictAnti` `Nat.instPreorder`	—	`RelEmbedding.not_wellFounded` `instIsStrictOrderLt` `wellFounded_lt`
`not_strictMono_of_wellFoundedGT` 📖	mathematical	—	`StrictMono` `Nat.instPreorder`	—	`not_strictAnti_of_wellFoundedLT` `instWellFoundedLTOrderDualOfWellFoundedGT`
`wellFoundedGT_iff_monotone_chain_condition` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike`	—	`wellFoundedGT_iff_monotone_chain_condition'` `lt_iff_le_and_ne` `OrderHom.mono`
`wellFoundedGT_iff_monotone_chain_condition'` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike`	—	`WellFounded.has_min` `IsWellFounded.wf` `Set.range_nonempty` `Set.mem_range_self` `WellFoundedGT.eq_1` `isWellFounded_iff` `RelEmbedding.wellFounded_iff_isEmpty` `instIsStrictOrderGt` `LT.lt.le` `RelEmbedding.map_rel_iff`

---

← Back to Index