Colex

📁 Source: Mathlib/Combinatorics/Colex.lean

Statistics

Metric	Count
Definitions `Colex`, `IsInitSeg`, `initSeg`, `instBoundedOrder`, `instDecidableLE`, `instDecidableLT`, `instLE`, `instLinearOrder`, `instOrderBot`, `instPartialOrder`, `equivBitIndices`, `instInhabitedColex`, `orderIsoColex`	13
Theorems `exists_initSeg`, `total`, `cons_le_cons`, `cons_lt_cons`, `erase_le_erase`, `erase_le_erase_min'`, `erase_lt_erase`, `forall_le_mono`, `forall_lt_mono`, `initSeg_nonempty`, `insert_le_insert`, `insert_lt_insert`, `isInitSeg_empty`, `isInitSeg_iff_exists_initSeg`, `isInitSeg_initSeg`, `le_def`, `le_iff_max'_mem`, `le_iff_sdiff_subset_lowerClosure`, `lt_iff_exists_filter_lt`, `lt_iff_exists_forall_lt`, `lt_iff_max'_mem`, `mem_initSeg`, `mem_initSeg_self`, `ofColex_bot`, `ofColex_top`, `singleton_le_singleton`, `singleton_le_toColex`, `singleton_lt_singleton`, `toColex_empty`, `toColex_image_le_toColex_image`, `toColex_image_lt_toColex_image`, `toColex_image_ofColex_strictMono`, `toColex_le_singleton`, `toColex_le_toColex`, `toColex_le_toColex_iff_max'_mem`, `toColex_le_toColex_of_subset`, `toColex_lt_singleton`, `toColex_lt_toColex`, `toColex_lt_toColex_iff_exists_forall_lt`, `toColex_lt_toColex_iff_max'_mem`, `toColex_lt_toColex_of_ssubset`, `toColex_mono`, `toColex_sdiff_le_toColex_sdiff`, `toColex_sdiff_le_toColex_sdiff'`, `toColex_sdiff_lt_toColex_sdiff`, `toColex_sdiff_lt_toColex_sdiff'`, `toColex_strictMono`, `toColex_univ`, `equivBitIndices_apply`, `equivBitIndices_symm_apply`, `geomSum_injective`, `geomSum_le_geomSum_iff_toColex_le_toColex`, `geomSum_lt_geomSum_iff_toColex_lt_toColex`, `geomSum_ofColex_strictMono`, `lt_geomSum_of_mem`, `orderIsoColex_apply`, `orderIsoColex_symm_apply`, `toFinset_bitIndices_twoPowSum`, `twoPowSum_toFinset_bitIndices`	59
Total	72

Finset

Definitions

Name	Category	Theorems
`equivBitIndices` 📖	CompOp	4 math math: `equivBitIndices_apply`, `equivBitIndices_symm_apply`, `orderIsoColex_symm_apply`, `orderIsoColex_apply`
`instInhabitedColex` 📖	CompOp	—
`orderIsoColex` 📖	CompOp	2 math math: `orderIsoColex_symm_apply`, `orderIsoColex_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivBitIndices_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivBitIndices` `List.toFinset` `Nat.bitIndices`	—	—
`equivBitIndices_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivBitIndices` `sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid`	—	—
`geomSum_injective` 📖	mathematical	—	`Finset` `sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid`	—	`le_antisymm_iff` `geomSum_le_geomSum_iff_toColex_le_toColex`
`geomSum_le_geomSum_iff_toColex_le_toColex` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid` `Colex` `Finset` `Colex.instLE` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`StrictMono.le_iff_le` `geomSum_ofColex_strictMono`
`geomSum_lt_geomSum_iff_toColex_lt_toColex` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid` `Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `Colex.instPartialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`StrictMono.lt_iff_lt` `geomSum_ofColex_strictMono`
`geomSum_ofColex_strictMono` 📖	mathematical	—	`StrictMono` `Colex` `Finset` `PartialOrder.toPreorder` `Colex.instPartialOrder` `Nat.instPartialOrder` `Nat.instPreorder` `sum` `Nat.instAddCommMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Monoid.toPow` `Nat.instMonoid`	—	`Colex.lt_iff_exists_forall_lt` `sum_sdiff_lt_sum_sdiff` `Nat.instIsOrderedCancelAddMonoid` `LT.lt.trans_le` `Nat.geomSum_lt` `single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mem_sdiff`
`lt_geomSum_of_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid`	—	`LT.lt.trans_le` `single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instCanonicallyOrderedAdd`
`orderIsoColex_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Colex` `Finset` `Colex.instLE` `Nat.instPartialOrder` `RelIso.instFunLike` `orderIsoColex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `equivBitIndices`	—	—
`orderIsoColex_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Colex` `Finset` `Colex.instLE` `Nat.instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `orderIsoColex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivBitIndices` `ofColex`	—	—
`toFinset_bitIndices_twoPowSum` 📖	mathematical	—	`List.toFinset` `Nat.bitIndices` `sum` `Nat.instAddCommMonoid` `Monoid.toPow` `Nat.instMonoid`	—	`geomSum_injective` `Eq.le` `List.sum_toFinset` `List.SortedLT.nodup` `Nat.bitIndices_sorted` `Nat.twoPowSum_bitIndices`
`twoPowSum_toFinset_bitIndices` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `List.toFinset` `Nat.bitIndices` `Monoid.toPow` `Nat.instMonoid`	—	`List.sum_toFinset` `List.SortedLT.nodup` `Nat.bitIndices_sorted` `Nat.twoPowSum_bitIndices`

Finset.Colex

Definitions

Name	Category	Theorems
`IsInitSeg` 📖	MathDef	5 math math: `Finset.UV.isInitSeg_of_compressed`, `isInitSeg_iff_exists_initSeg`, `IsInitSeg.shadow`, `isInitSeg_empty`, `isInitSeg_initSeg`
`initSeg` 📖	CompOp	7 math math: `mem_initSeg_self`, `mem_initSeg`, `IsInitSeg.exists_initSeg`, `isInitSeg_iff_exists_initSeg`, `shadow_initSeg`, `initSeg_nonempty`, `isInitSeg_initSeg`
`instBoundedOrder` 📖	CompOp	2 math math: `toColex_univ`, `ofColex_top`
`instDecidableLE` 📖	CompOp	—
`instDecidableLT` 📖	CompOp	—
`instLE` 📖	CompOp	24 math math: `toColex_le_singleton`, `toColex_univ`, `le_iff_max'_mem`, `toColex_sdiff_le_toColex_sdiff'`, `mem_initSeg`, `Finset.geomSum_le_geomSum_iff_toColex_le_toColex`, `erase_le_erase`, `toColex_le_toColex_iff_max'_mem`, `singleton_le_toColex`, `toColex_sdiff_le_toColex_sdiff`, `ofColex_top`, `toColex_le_toColex`, `insert_le_insert`, `le_def`, `erase_le_erase_min'`, `singleton_le_singleton`, `toColex_image_le_toColex_image`, `toColex_empty`, `le_iff_sdiff_subset_lowerClosure`, `cons_le_cons`, `Finset.orderIsoColex_symm_apply`, `toColex_le_toColex_of_subset`, `Finset.orderIsoColex_apply`, `ofColex_bot`
`instLinearOrder` 📖	CompOp	—
`instOrderBot` 📖	CompOp	2 math math: `toColex_empty`, `ofColex_bot`
`instPartialOrder` 📖	CompOp	21 math math: `Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex`, `toColex_lt_toColex_iff_max'_mem`, `cons_lt_cons`, `lt_iff_exists_forall_lt`, `toColex_strictMono`, `erase_lt_erase`, `toColex_image_lt_toColex_image`, `toColex_sdiff_lt_toColex_sdiff`, `Finset.geomSum_ofColex_strictMono`, `lt_iff_exists_filter_lt`, `toColex_lt_singleton`, `singleton_lt_singleton`, `toColex_lt_toColex_iff_exists_forall_lt`, `toColex_mono`, `Finset.UV.toColex_compress_lt_toColex`, `lt_iff_max'_mem`, `toColex_lt_toColex_of_ssubset`, `toColex_image_ofColex_strictMono`, `toColex_lt_toColex`, `toColex_sdiff_lt_toColex_sdiff'`, `insert_lt_insert`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_le_cons` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.cons` `Preorder.toLE` `PartialOrder.toPreorder`	—	`eq_or_ne` `instReflLe` `toColex_sdiff_le_toColex_sdiff'` `Finset.cons_sdiff_cons` `singleton_le_singleton`
`cons_lt_cons` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.cons`	—	`lt_iff_lt_of_le_iff_le'` `cons_le_cons`
`erase_le_erase` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.erase` `Preorder.toLE` `PartialOrder.toPreorder`	—	`eq_or_ne` `instReflLe` `toColex_sdiff_le_toColex_sdiff'` `Finset.erase_sdiff_erase` `singleton_le_singleton`
`erase_le_erase_min'` 📖	mathematical	`Colex` `Finset` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.card` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.erase` `LinearOrder.toDecidableEq` `Finset.min'` `Finset.card` `Finset.Nonempty` `Finset.card_pos` `LT.lt.trans_le` `Nat.instPreorder` `SetLike.instMembership` `Finset.instSetLike`	—	`eq_or_ne` `erase_le_erase` `Finset.min'_mem` `Finset.min'_le` `LE.le.lt_of_ne` `Iff.not` `Ne.lt_or_gt` `LE.le.trans_lt` `LT.lt.le` `lt_iff_exists_forall_lt` `Finset.mem_erase` `LT.lt.ne'` `Finset.notMem_erase` `not_ne_iff` `not_and_or` `LT.lt.trans_le` `Finset.mem_of_mem_erase` `LE.le.eq_or_lt` `Ne.lt_of_le'` `Finset.eq_of_subset_of_card_le` `Finset.card_erase_of_mem` `tsub_le_tsub_right` `Nat.instOrderedSub` `le_refl` `Finset.card_pos`
`erase_lt_erase` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.erase`	—	`lt_iff_lt_of_le_iff_le'` `erase_le_erase`
`forall_le_mono` 📖	mathematical	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Preorder.toLE` `PartialOrder.toPreorder` `SetLike.instMembership` `Finset.instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder`	—	`LE.le.trans`
`forall_lt_mono` 📖	mathematical	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Preorder.toLT` `PartialOrder.toPreorder` `SetLike.instMembership` `Finset.instSetLike`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.trans_lt`
`initSeg_nonempty` 📖	mathematical	—	`Finset.Nonempty` `Finset` `initSeg`	—	`mem_initSeg_self`
`insert_le_insert` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instInsert` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Finset.cons_eq_insert` `cons_le_cons`
`insert_lt_insert` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instInsert`	—	`Finset.cons_eq_insert` `cons_lt_cons`
`isInitSeg_empty` 📖	mathematical	—	`IsInitSeg` `Finset` `Finset.instEmptyCollection`	—	`Finset.coe_empty` `instIsEmptyFalse`
`isInitSeg_iff_exists_initSeg` 📖	mathematical	—	`IsInitSeg` `Finset.Nonempty` `Finset` `Finset.card` `initSeg`	—	`IsInitSeg.exists_initSeg` `isInitSeg_initSeg` `initSeg_nonempty`
`isInitSeg_initSeg` 📖	mathematical	—	`IsInitSeg` `initSeg` `Finset.card`	—	`mem_initSeg` `LE.le.trans` `LT.lt.le`
`le_def` 📖	mathematical	—	`Colex` `Finset` `instLE` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Preorder.toLE` `PartialOrder.toPreorder`	—	—
`le_iff_max'_mem` 📖	mathematical	—	`Colex` `Finset` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Finset.max'` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `LinearOrder.toDecidableEq` `Finset.instSDiff`	—	`toColex_le_toColex_iff_max'_mem`
`le_iff_sdiff_subset_lowerClosure` 📖	mathematical	—	`Colex` `Finset` `instLE` `Set` `Set.instHasSubset` `Set.instSDiff` `SetLike.coe` `Finset.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure`	—	—
`lt_iff_exists_filter_lt` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike` `Finset.instSDiff` `LinearOrder.toDecidableEq` `Finset.filter` `LinearOrder.toDecidableLT`	—	`Finset.max'_mem` `not_imp_comm` `LT.lt.asymm` `LT.lt.trans` `LT.lt.not_ge` `Finset.le_max'` `LE.le.lt_of_ne`
`lt_iff_exists_forall_lt` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	`toColex_lt_toColex_iff_exists_forall_lt`
`lt_iff_max'_mem` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Finset.max'` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `LinearOrder.toDecidableEq` `Finset.instSDiff`	—	`lt_iff_le_and_ne` `le_iff_max'_mem`
`mem_initSeg` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `initSeg` `Finset.card` `Colex` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	—
`mem_initSeg_self` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `initSeg`	—	`instReflLe`
`ofColex_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Colex` `Finset` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Bot.bot` `OrderBot.toBot` `instLE` `instOrderBot` `Finset.instEmptyCollection`	—	—
`ofColex_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Colex` `Finset` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Top.top` `OrderTop.toTop` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BoundedOrder.toOrderTop` `instBoundedOrder` `Finset.univ`	—	—
`singleton_le_singleton` 📖	mathematical	—	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSingleton` `Preorder.toLE` `PartialOrder.toPreorder`	—	—
`singleton_le_toColex` 📖	mathematical	—	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSingleton` `SetLike.instMembership` `Finset.instSetLike` `Preorder.toLE` `PartialOrder.toPreorder`	—	`instIsEmptyFalse` `le_refl`
`singleton_lt_singleton` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSingleton`	—	—
`toColex_empty` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `Colex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instEmptyCollection` `Bot.bot` `OrderBot.toBot` `instLE` `instOrderBot`	—	—
`toColex_image_le_toColex_image` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Colex` `Finset` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.image` `LinearOrder.toDecidableEq`	—	`StrictMono.injective` `StrictMono.le_iff_le`
`toColex_image_lt_toColex_image` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.image` `LinearOrder.toDecidableEq`	—	`lt_iff_lt_of_le_iff_le` `toColex_image_le_toColex_image`
`toColex_image_ofColex_strictMono` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`StrictMono` `Colex` `Finset` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.image` `LinearOrder.toDecidableEq` `ofColex`	—	`toColex_image_lt_toColex_image`
`toColex_le_singleton` 📖	mathematical	—	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSingleton` `Preorder.toLE` `PartialOrder.toPreorder`	—	`eq_or_ne` `instReflLe`
`toColex_le_toColex` 📖	mathematical	—	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike` `Preorder.toLE` `PartialOrder.toPreorder`	—	—
`toColex_le_toColex_iff_max'_mem` 📖	mathematical	—	`Colex` `Finset` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike` `Finset.max'` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `LinearOrder.toDecidableEq` `Finset.instSDiff` `Finset.Nonempty` `Finset.symmDiff_nonempty`	—	`Finset.symmDiff_nonempty` `Finset.max'_mem` `lt_irrefl` `Finset.max'_lt_iff` `LE.le.lt_of_ne` `Finset.mem_symmDiff` `Finset.le_max'`
`toColex_le_toColex_of_subset` 📖	mathematical	`Finset` `Finset.instHasSubset`	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toColex_mono`
`toColex_lt_singleton` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSingleton`	—	`lt_iff_le_and_ne` `toColex_le_singleton` `LE.le.lt_of_ne` `Finset.eq_singleton_iff_unique_mem` `LT.lt.le` `lt_irrefl`
`toColex_lt_toColex` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike` `Preorder.toLE`	—	`EquivLike.toEmbeddingLike`
`toColex_lt_toColex_iff_exists_forall_lt` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike`	—	`not_le` `toColex_le_toColex`
`toColex_lt_toColex_iff_max'_mem` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `SetLike.instMembership` `Finset.instSetLike` `Finset.max'` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Finset.instLattice` `LinearOrder.toDecidableEq` `Finset.instSDiff` `Finset.Nonempty` `Finset.symmDiff_nonempty`	—	`Finset.symmDiff_nonempty` `lt_iff_le_and_ne` `toColex_le_toColex_iff_max'_mem` `EquivLike.toEmbeddingLike`
`toColex_lt_toColex_of_ssubset` 📖	mathematical	`Finset` `Finset.instHasSSubset`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toColex_strictMono`
`toColex_mono` 📖	mathematical	—	`Monotone` `Finset` `Colex` `PartialOrder.toPreorder` `Finset.partialOrder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	—
`toColex_sdiff_le_toColex_sdiff` 📖	mathematical	`Finset` `Finset.instHasSubset`	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSDiff`	—	`sdiff_sdiff_sdiff_cancel_right`
`toColex_sdiff_le_toColex_sdiff'` 📖	mathematical	—	`Colex` `Finset` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSDiff`	—	`Finset.sdiff_inter_self_left` `Finset.sdiff_inter_self_right` `toColex_sdiff_le_toColex_sdiff` `Finset.inter_subset_left` `Finset.inter_subset_right`
`toColex_sdiff_lt_toColex_sdiff` 📖	mathematical	`Finset` `Finset.instHasSubset`	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSDiff`	—	`lt_iff_lt_of_le_iff_le'` `toColex_sdiff_le_toColex_sdiff`
`toColex_sdiff_lt_toColex_sdiff'` 📖	mathematical	—	`Colex` `Finset` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.instSDiff`	—	`Finset.sdiff_inter_self_left` `Finset.sdiff_inter_self_right` `toColex_sdiff_lt_toColex_sdiff` `Finset.inter_subset_left` `Finset.inter_subset_right`
`toColex_strictMono` 📖	mathematical	—	`StrictMono` `Finset` `Colex` `PartialOrder.toPreorder` `Finset.partialOrder` `instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`Monotone.strictMono_of_injective` `toColex_mono` `Equiv.injective`
`toColex_univ` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `Colex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finset.univ` `Top.top` `OrderTop.toTop` `instLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BoundedOrder.toOrderTop` `instBoundedOrder`	—	—

Finset.Colex.IsInitSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_initSeg` 📖	mathematical	`Finset.Colex.IsInitSeg` `Finset.Nonempty` `Finset`	`Finset` `Finset.card` `Finset.Colex.initSeg`	—	`Finset.sup'_mem` `LinearOrder.supClosed` `Finset.ext` `Finset.Colex.mem_initSeg` `Finset.le_sup'` `LE.le.eq_or_lt`
`total` 📖	mathematical	`Finset.Colex.IsInitSeg`	`Finset` `Finset.instHasSubset`	—	`trichotomous_of` `instTrichotomousLt` `Finset.mem_sdiff`

(root)

Definitions

Name	Category	Theorems
`Colex` 📖	CompOp	159 math math: `toColex_symm_eq`, `instLawfulBEqColex`, `Finset.Colex.toColex_le_singleton`, `Finsupp.Colex.addLeftStrictMono`, `Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex`, `isLeftRegular_ofColex`, `toColex_ofColex`, `toColex_sub`, `Finset.Colex.toColex_univ`, `Finsupp.toColex_monotone`, `pow_toColex`, `Pi.toColex_monotone`, `ofColex_one`, `Pi.colex_asc`, `instIsRightCancelAddColex`, `DFinsupp.Colex.isOrderedCancelAddMonoid`, `toColex_vadd`, `Pi.Colex.lt_iff_of_unique`, `toColex_inv`, `toColex_add`, `Finset.Colex.toColex_lt_toColex_iff_max'_mem`, `Pi.Colex.le_sSup_apply`, `Finsupp.Colex.isOrderedCancelAddMonoid`, `Finset.Colex.le_iff_max'_mem`, `Finsupp.Colex.isStrictOrder`, `Finset.Colex.cons_lt_cons`, `Finset.Colex.toColex_sdiff_le_toColex_sdiff'`, `Colex.forall`, `ofColex_div`, `DFinsupp.Colex.wellFoundedLT`, `ofColex_add`, `Finset.Colex.lt_iff_exists_forall_lt`, `DFinsupp.Colex.addRightMono`, `Finset.Colex.toColex_strictMono`, `isAddRightRegular_toColex`, `Pi.Colex.sSup_apply`, `Finset.Colex.mem_initSeg`, `Finset.geomSum_le_geomSum_iff_toColex_le_toColex`, `Finset.Colex.erase_lt_erase`, `Finset.Colex.erase_le_erase`, `isAddLeftRegular_ofColex`, `Finset.Colex.toColex_le_toColex_iff_max'_mem`, `ofColex_vadd'`, `Pi.colex_le_iff_of_unique`, `pow_ofColex`, `Finsupp.Colex.addRightMono`, `ofColex_smul'`, `Finset.Colex.singleton_le_toColex`, `Finsupp.Colex.wellFoundedLT`, `Finset.Colex.toColex_image_lt_toColex_image`, `Finsupp.Colex.addRightStrictMono`, `Pi.Colex.noMaxOrder'`, `isAddRegular_ofColex`, `instNonemptyColex`, `toColex_eq_zero`, `Finset.Colex.toColex_sdiff_lt_toColex_sdiff`, `Pi.ofColex_apply`, `Finset.Colex.toColex_sdiff_le_toColex_sdiff`, `DFinsupp.colex_lt_iff_of_unique`, `Finset.geomSum_ofColex_strictMono`, `ofColex_mul`, `Finsupp.Colex.wellFoundedLT_of_finite`, `ofColex_eq_zero`, `isRightRegular_toColex`, `toColex_one`, `ofColex_inv`, `DFinsupp.Colex.le_iff_of_unique`, `Finset.Colex.ofColex_top`, `DFinsupp.Colex.lt_iff`, `instIsCancelMulColex`, `Finset.Colex.lt_iff_exists_filter_lt`, `Finset.Colex.toColex_le_toColex`, `Pi.Colex.isStrictOrder`, `Finset.Colex.toColex_lt_singleton`, `Finset.Colex.singleton_lt_singleton`, `Pi.Colex.sSup_apply_le`, `Pi.lt_toColex_update_self_iff`, `toColex_neg`, `Finsupp.Colex.le_iff_of_unique`, `toColex_smul`, `toColex_vadd'`, `Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt`, `Pi.Colex.sInf_apply_le`, `Finset.Colex.insert_le_insert`, `ofColex_inj`, `Finset.Colex.toColex_mono`, `ofColex_smul`, `toColex_inj`, `Finsupp.Colex.lt_iff`, `instNontrivialColex`, `Pi.toColex_apply`, `instIsRightCancelMulColex`, `ofColex_symm_eq`, `ofColex_vadd`, `isAddRightRegular_ofColex`, `Pi.Colex.le_sInf_apply`, `Finset.Colex.le_def`, `Pi.instDenselyOrderedColexForall`, `Finset.UV.toColex_compress_lt_toColex`, `toColex_mul`, `Pi.toColex_strictMono`, `ofColex_pow`, `Finset.Colex.lt_iff_max'_mem`, `Finset.Colex.erase_le_erase_min'`, `Pi.Colex.wellFoundedLT`, `DFinsupp.Colex.wellFoundedLT_of_finite`, `isRightRegular_ofColex`, `Pi.toColex_update_le_self_iff`, `instIsCancelAddColex`, `Finsupp.Colex.addLeftMono`, `Finset.Colex.toColex_lt_toColex_of_ssubset`, `Colex.exists`, `ofColex_eq_one`, `Finset.Colex.toColex_image_ofColex_strictMono`, `DFinsupp.Colex.total_le`, `DFinsupp.toColex_monotone`, `ofColex_sub`, `Pi.instNoMaxOrderColexForallOfWellFoundedGTOfNonempty`, `instIsLeftCancelMulColex`, `isAddRegular_toColex`, `DFinsupp.Colex.addLeftStrictMono`, `Finset.Colex.singleton_le_singleton`, `Finset.Colex.toColex_lt_toColex`, `Finset.Colex.toColex_image_le_toColex_image`, `Finset.Colex.toColex_sdiff_lt_toColex_sdiff'`, `Finset.Colex.toColex_empty`, `DFinsupp.Colex.addRightStrictMono`, `Finsupp.Colex.single_le_iff`, `Pi.instNoMinOrderColexForallOfWellFoundedGTOfNonempty`, `Finset.Colex.le_iff_sdiff_subset_lowerClosure`, `Finset.Colex.cons_le_cons`, `toColex_zero`, `toColex_div`, `Pi.le_toColex_update_self_iff`, `DFinsupp.Colex.isOrderedAddMonoid`, `Pi.Colex.sInf_apply`, `toColex_pow`, `isAddLeftRegular_toColex`, `ofColex_neg`, `DFinsupp.Colex.addLeftMono`, `Finsupp.Colex.single_lt_iff`, `Pi.colex_lt_iff_of_unique`, `ofColex_toColex`, `isRegular_toColex`, `Finset.orderIsoColex_symm_apply`, `toColex_eq_one`, `Finset.Colex.toColex_le_toColex_of_subset`, `Finsupp.Colex.lt_iff_of_unique`, `DFinsupp.Colex.isStrictOrder`, `ofColex_zero`, `Finset.orderIsoColex_apply`, `Finset.Colex.insert_lt_insert`, `toColex_smul'`, `Finset.Colex.ofColex_bot`, `Finsupp.Colex.single_strictMono`, `isRegular_ofColex`, `Pi.toColex_update_lt_self_iff`, `isLeftRegular_toColex`, `instIsLeftCancelAddColex`

---

← Back to Index