Height

Statistics

Metric	Count
Definitions `chainHeight`	1
Theorems `chainHeight_coe_univ`, `chainHeight_coe_univ_le`, `chainHeight_coe_univ_lt`, `chainHeight_empty`, `chainHeight_eq_iSup`, `chainHeight_eq_of_relEmbedding`, `chainHeight_eq_of_relIso`, `chainHeight_eq_top_iff`, `chainHeight_eq_zero_iff`, `chainHeight_flip`, `chainHeight_le_encard`, `chainHeight_mono`, `chainHeight_ne_top_of_finite`, `chainHeight_of_isEmpty`, `encard_eq_chainHeight_of_isChain`, `encard_le_chainHeight_of_isChain`, `exists_eq_chainHeight_of_chainHeight_ne_top`, `exists_eq_chainHeight_of_finite`, `exists_isChain_of_le_chainHeight`, `finite_of_chainHeight_ne_top`, `not_isChain_of_chainHeight_lt_encard`, `one_le_chainHeight_iff`	22
Total	23

Set

Definitions

Name	Category	Theorems
`chainHeight` 📖	CompOp	18 math math: `chainHeight_eq_of_relEmbedding`, `chainHeight_le_encard`, `chainHeight_mono`, `exists_eq_chainHeight_of_chainHeight_ne_top`, `chainHeight_eq_of_relIso`, `chainHeight_coe_univ_lt`, `one_le_chainHeight_iff`, `chainHeight_empty`, `chainHeight_coe_univ_le`, `encard_le_chainHeight_of_isChain`, `chainHeight_flip`, `encard_eq_chainHeight_of_isChain`, `chainHeight_coe_univ`, `chainHeight_of_isEmpty`, `chainHeight_eq_iSup`, `chainHeight_eq_zero_iff`, `exists_eq_chainHeight_of_finite`, `chainHeight_eq_top_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chainHeight_coe_univ` 📖	mathematical	—	`chainHeight` `Elem` `univ` `Set` `instMembership`	—	`chainHeight_eq_of_relEmbedding` `image_congr` `image_univ` `Subtype.range_coe_subtype`
`chainHeight_coe_univ_le` 📖	mathematical	—	`chainHeight` `Elem` `univ` `Set` `instMembership`	—	`chainHeight_coe_univ`
`chainHeight_coe_univ_lt` 📖	mathematical	—	`chainHeight` `Elem` `univ` `Set` `instMembership`	—	`chainHeight_coe_univ`
`chainHeight_empty` 📖	mathematical	—	`chainHeight` `Set` `instEmptyCollection` `ENat` `instZeroENat`	—	`chainHeight_eq_zero_iff`
`chainHeight_eq_iSup` 📖	mathematical	—	`chainHeight` `iSup` `ENat` `Set` `instHasSubset` `IsChain` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `encard`	—	—
`chainHeight_eq_of_relEmbedding` 📖	mathematical	—	`chainHeight` `image` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike`	—	`ENat.eq_of_forall_natCast_le_iff` `exists_isChain_of_le_chainHeight` `encard_preimage_of_injective_subset_range` `RelEmbedding.injective` `encard_le_chainHeight_of_isChain` `preimage_subset` `Function.Injective.injOn` `IsChain.preimage_relEmbedding` `Function.Injective.encard_image` `IsChain.image_relEmbedding`
`chainHeight_eq_of_relIso` 📖	mathematical	—	`chainHeight` `image` `DFunLike.coe` `RelIso` `RelIso.instFunLike`	—	`chainHeight_eq_of_relEmbedding`
`chainHeight_eq_top_iff` 📖	mathematical	—	`chainHeight` `Top.top` `ENat` `instTopENat` `Set` `instHasSubset` `encard` `ENat.instNatCast` `IsChain`	—	`exists_isChain_of_le_chainHeight` `LE.le.trans_eq` `le_top` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `WithTop.ne_top_iff_exists` `not_isChain_of_chainHeight_lt_encard` `ENat.some_eq_coe` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid`
`chainHeight_eq_zero_iff` 📖	mathematical	—	`chainHeight` `ENat` `instZeroENat` `Set` `instEmptyCollection`	—	`ext`
`chainHeight_flip` 📖	mathematical	—	`chainHeight`	—	`ENat.eq_of_forall_natCast_le_iff` `exists_isChain_of_le_chainHeight` `encard_le_chainHeight_of_isChain`
`chainHeight_le_encard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chainHeight` `encard`	—	—
`chainHeight_mono` 📖	mathematical	`Set` `instHasSubset`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chainHeight`	—	`ENat.forall_natCast_le_iff_le` `exists_isChain_of_le_chainHeight` `encard_le_chainHeight_of_isChain` `HasSubset.Subset.trans` `instIsTransSubset`
`chainHeight_ne_top_of_finite` 📖	—	—	—	—	`LT.lt.ne_top` `lt_of_le_of_lt` `chainHeight_le_encard` `lt_top_iff_ne_top` `encard_ne_top_iff`
`chainHeight_of_isEmpty` 📖	mathematical	—	`chainHeight` `ENat` `instZeroENat`	—	`chainHeight_eq_zero_iff` `Unique.instSubsingleton`
`encard_eq_chainHeight_of_isChain` 📖	mathematical	`IsChain`	`encard` `chainHeight`	—	`le_antisymm` `encard_le_chainHeight_of_isChain` `Subset.rfl` `chainHeight_le_encard`
`encard_le_chainHeight_of_isChain` 📖	mathematical	`Set` `instHasSubset` `IsChain`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `encard` `chainHeight`	—	`le_iSup_iff`
`exists_eq_chainHeight_of_chainHeight_ne_top` 📖	mathematical	—	`Set` `instHasSubset` `encard` `chainHeight` `IsChain`	—	`ENat.exists_eq_iSup_of_lt_top` `chainHeight_eq_iSup` `lt_top_iff_ne_top`
`exists_eq_chainHeight_of_finite` 📖	mathematical	—	`Set` `instHasSubset` `encard` `chainHeight` `IsChain`	—	`exists_eq_chainHeight_of_chainHeight_ne_top` `chainHeight_ne_top_of_finite`
`exists_isChain_of_le_chainHeight` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `chainHeight`	`Set` `instHasSubset` `encard` `IsChain`	—	`encard_empty` `Nat.cast_zero` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `iSup_lt_iff` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENat.le_sub_one_of_lt` `exists_subset_encard_eq` `HasSubset.Subset.trans` `instIsTransSubset` `IsChain.mono`
`finite_of_chainHeight_ne_top` 📖	mathematical	`IsChain`	`Finite`	—	`encard_ne_top_iff` `ne_top_of_le_ne_top` `encard_le_chainHeight_of_isChain` `subset_refl` `instReflSubset`
`not_isChain_of_chainHeight_lt_encard` 📖	mathematical	`Set` `instHasSubset` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chainHeight` `encard`	`IsChain`	—	`lt_self_iff_false` `lt_imp_lt_of_le_of_le` `le_refl` `encard_le_chainHeight_of_isChain`
`one_le_chainHeight_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `chainHeight` `Nonempty`	—	`chainHeight_empty` `NeZero.one`

---

← Back to Index