Lattice

📁 Source: Mathlib/Data/ENat/Lattice.lean

Statistics

Metric	Count
Definitions `instCompleteLinearOrderENat`, `instCompleteLinearOrderWithBotENat`	2
Theorems `add_biSup`, `add_biSup'`, `add_iInf`, `add_iInf₂`, `add_iSup`, `add_sInf`, `add_sSup`, `biSup_add`, `biSup_add'`, `biSup_add_biSup_le`, `biSup_add_biSup_le'`, `coe_iInf`, `coe_iSup`, `coe_sInf`, `coe_sSup`, `exists_eq_iInf`, `exists_eq_iSup_of_lt_top`, `exists_eq_iSup₂_of_lt_top`, `finite_of_sSup_lt_top`, `iInf_add`, `iInf_add_iInf`, `iInf_add_iInf_of_monotone`, `iInf_coe_eq_top`, `iInf_coe_lt_top`, `iInf_coe_ne_top`, `iInf_eq_top_of_isEmpty`, `iInf_eq_zero`, `iInf_mul`, `iInf_mul'`, `iInf_mul_of_ne`, `iInf_toNat`, `iInf₂_add`, `iSup_add`, `iSup_add_iSup`, `iSup_add_iSup_le`, `iSup_add_iSup_of_monotone`, `iSup_coe_eq_top`, `iSup_coe_lt_top`, `iSup_coe_ne_top`, `iSup_eq_zero`, `iSup_mul`, `iSup_natCast`, `iSup_zero`, `le_iInf_add_iInf`, `le_iInf₂_add_iInf₂`, `mul_iInf`, `mul_iInf'`, `mul_iInf_of_ne`, `mul_iSup`, `mul_sSup`, `sInf_add`, `sInf_eq_zero`, `sSup_add`, `sSup_eq_top_of_infinite`, `sSup_eq_zero`, `sSup_eq_zero'`, `sSup_mem_of_nonempty_of_lt_top`, `sSup_mul`, `smul_iSup`, `smul_sSup`, `sub_iInf`, `sub_iSup`	62
Total	64

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_biSup` 📖	mathematical	`Set.Nonempty`	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership`	—	`add_biSup'`
`add_biSup'` 📖	mathematical	—	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iSup_subtype'` `add_iSup` `nonempty_subtype`
`add_iInf` 📖	mathematical	—	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`add_comm` `iInf_add`
`add_iInf₂` 📖	mathematical	—	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`add_iInf`
`add_iSup` 📖	mathematical	—	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`eq_or_ne` `top_add` `ciSup_const` `le_antisymm` `add_le_of_le_tsub_left_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_iSup_of_le` `le_self_add` `iSup_le` `le_sub_of_add_le_left` `le_iSup` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right`
`add_sInf` 📖	mathematical	—	`ENat` `instAddENat` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iInf` `Set` `Set.instMembership`	—	`sInf_eq_iInf` `add_iInf₂`
`add_sSup` 📖	mathematical	`Set.Nonempty` `ENat`	`ENat` `instAddENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `add_biSup`
`biSup_add` 📖	mathematical	`Set.Nonempty`	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership`	—	`biSup_add'`
`biSup_add'` 📖	mathematical	—	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`add_comm` `add_biSup'` `iSup_congr_Prop`
`biSup_add_biSup_le` 📖	mathematical	`Set.Nonempty` `ENat` `instLEENat` `instAddENat`	`ENat` `instLEENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership`	—	`biSup_add_biSup_le'`
`biSup_add_biSup_le'` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instLEENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`biSup_add'` `iSup_congr_Prop` `add_biSup'` `iSup₂_le`
`coe_iInf` 📖	mathematical	—	`ENat` `instNatCast` `iInf` `Nat.instInfSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`WithTop.coe_iInf` `OrderBot.bddBelow`
`coe_iSup` 📖	mathematical	`BddAbove` `Set.range`	`ENat` `instNatCast` `iSup` `Nat.instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`WithTop.coe_iSup`
`coe_sInf` 📖	mathematical	`Set.Nonempty`	`ENat` `instNatCast` `InfSet.sInf` `Nat.instInfSet` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership`	—	`WithTop.coe_sInf` `OrderBot.bddBelow`
`coe_sSup` 📖	mathematical	`BddAbove`	`ENat` `instNatCast` `SupSet.sSup` `Nat.instSupSet` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set` `Set.instMembership`	—	`WithTop.coe_sSup`
`exists_eq_iInf` 📖	mathematical	—	`iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`csInf_mem` `Set.range_nonempty`
`exists_eq_iSup_of_lt_top` 📖	mathematical	`ENat` `instLTENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `instTopENat`	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`sSup_mem_of_nonempty_of_lt_top` `Set.instNonemptyRange`
`exists_eq_iSup₂_of_lt_top` 📖	mathematical	`ENat` `instLTENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `instTopENat`	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iSup_prod'` `Prod.exists'` `exists_eq_iSup_of_lt_top`
`finite_of_sSup_lt_top` 📖	mathematical	`ENat` `instLTENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `instTopENat`	`Set.Finite` `ENat`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `sSup_eq_top_of_infinite`
`iInf_add` 📖	mathematical	—	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`le_antisymm` `le_iInf` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `iInf_le` `le_rfl` `tsub_le_iff_right`
`iInf_add_iInf` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`le_iInf₂` `iInf_le_of_le` `iInf_add` `add_iInf` `le_antisymm` `le_iInf` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `iInf_le`
`iInf_add_iInf_of_monotone` 📖	mathematical	`Monotone` `ENat` `instPreorderENat`	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iInf_add_iInf` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `exists_le_le`
`iInf_coe_eq_top` 📖	mathematical	—	`iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat` `IsEmpty`	—	`WithTop.iInf_coe_eq_top`
`iInf_coe_lt_top` 📖	mathematical	—	`ENat` `instLTENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat`	—	`WithTop.iInf_coe_lt_top`
`iInf_coe_ne_top` 📖	—	—	—	—	`iInf_coe_eq_top` `not_isEmpty_iff`
`iInf_eq_top_of_isEmpty` 📖	mathematical	—	`iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat`	—	`iInf_coe_eq_top`
`iInf_eq_zero` 📖	mathematical	—	`iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`iInf_lt_iff`
`iInf_mul` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`mul_comm` `mul_iInf`
`iInf_mul'` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`mul_comm` `mul_iInf'`
`iInf_mul_of_ne` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iInf_mul'` `instIsEmptyFalse`
`iInf_toNat` 📖	mathematical	—	`toNat` `iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Nat.instInfSet`	—	`isEmpty_or_nonempty` `iInf_eq_top_of_isEmpty` `Nat.iInf_of_empty`
`iInf₂_add` 📖	mathematical	—	`ENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`add_comm` `add_iInf₂`
`iSup_add` 📖	mathematical	—	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`add_comm` `add_iSup`
`iSup_add_iSup` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`isEmpty_or_nonempty` `iSup_of_empty` `bot_eq_zero` `zero_add` `le_antisymm` `iSup_add_iSup_le` `le_iSup_of_le` `iSup_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_iSup`
`iSup_add_iSup_le` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instLEENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iSup_add` `add_iSup` `iSup₂_le`
`iSup_add_iSup_of_monotone` 📖	mathematical	`Monotone` `ENat` `instPreorderENat`	`ENat` `instAddENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iSup_add_iSup` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `exists_ge_ge`
`iSup_coe_eq_top` 📖	mathematical	—	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat` `BddAbove` `Set.range`	—	`WithTop.iSup_coe_eq_top`
`iSup_coe_lt_top` 📖	mathematical	—	`ENat` `instLTENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat` `BddAbove` `Set.range`	—	`WithTop.iSup_coe_lt_top`
`iSup_coe_ne_top` 📖	mathematical	—	`BddAbove` `Set.range`	—	`Iff.not_left` `iSup_coe_eq_top`
`iSup_eq_zero` 📖	mathematical	—	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`iSup_eq_bot`
`iSup_mul` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`mul_comm` `mul_iSup`
`iSup_natCast` 📖	mathematical	—	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instNatCast` `Top.top` `instTopENat`	—	`iSup_eq_top` `exists_nat_gt` `lt_top_iff_ne_top`
`iSup_zero` 📖	mathematical	—	`iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	—
`le_iInf_add_iInf` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instLEENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iInf_add` `add_iInf` `le_iInf₂`
`le_iInf₂_add_iInf₂` 📖	mathematical	`ENat` `instLEENat` `instAddENat`	`ENat` `instLEENat` `instAddENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`iInf₂_add` `add_iInf₂` `le_iInf₂`
`mul_iInf` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`LE.le.antisymm` `le_iInf` `le_imp_le_of_le_of_le` `mul_le_mul_right` `CanonicallyOrderedAdd.toMulLeftMono` `iInf_le` `le_refl` `exists_eq_iInf` `iInf_le_iff`
`mul_iInf'` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`isEmpty_or_nonempty` `iInf_of_empty` `mul_top'` `mul_iInf`
`mul_iInf_of_ne` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`mul_iInf'` `instIsEmptyFalse`
`mul_iSup` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`LE.le.antisymm'` `iSup_le` `mul_le_mul'` `CanonicallyOrderedAdd.toMulLeftMono` `covariant_swap_mul_of_covariant_mul` `Eq.le` `le_iSup_iff` `eq_or_ne` `MulZeroClass.zero_mul` `isEmpty_or_nonempty` `ciSup_of_empty` `bot_eq_zero'` `MulZeroClass.mul_zero` `lt_top_iff_ne_top` `iSup_eq_top` `LT.lt.false` `LT.lt.trans_le` `LE.le.trans_lt` `self_le_mul_left` `exists_eq_iSup_of_lt_top`
`mul_sSup` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `mul_iSup`
`sInf_add` 📖	mathematical	—	`ENat` `instAddENat` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iInf` `Set` `Set.instMembership`	—	`sInf_eq_iInf` `iInf_add`
`sInf_eq_zero` 📖	mathematical	—	`InfSet.sInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instMembership`	—	`lt_one_iff_eq_zero`
`sSup_add` 📖	mathematical	`Set.Nonempty` `ENat`	`ENat` `instAddENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `biSup_add`
`sSup_eq_top_of_infinite` 📖	mathematical	`Set.Infinite` `ENat`	`SupSet.sSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `instTopENat`	—	`sSup_eq_top` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Set.Finite.subset` `Finite.Set.finite_image` `Finite.of_fintype` `lt_of_le_of_lt` `toNat_le_of_le_coe` `LT.lt.ne_top`
`sSup_eq_zero` 📖	mathematical	—	`SupSet.sSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`sSup_eq_bot`
`sSup_eq_zero'` 📖	mathematical	—	`SupSet.sSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instEmptyCollection` `Set.instSingletonSet`	—	`sSup_eq_bot'`
`sSup_mem_of_nonempty_of_lt_top` 📖	mathematical	`ENat` `instLTENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `instTopENat`	`ENat` `Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`Set.Nonempty.csSup_mem` `Set.Nonempty.of_subtype` `finite_of_sSup_lt_top`
`sSup_mul` 📖	mathematical	—	`ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `Set` `Set.instMembership`	—	`mul_comm` `iSup_congr_Prop` `mul_sSup`
`smul_iSup` 📖	mathematical	—	`ENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`smul_one_mul` `mul_iSup`
`smul_sSup` 📖	mathematical	—	`ENat` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `smul_iSup`
`sub_iInf` 📖	mathematical	—	`ENat` `instSubENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`eq_of_forall_ge_iff` `tsub_le_iff_right` `add_comm` `iInf_add`
`sub_iSup` 📖	mathematical	—	`ENat` `instSubENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`em` `tsub_eq_zero_iff_le` `le_iSup_of_le` `LT.lt.le` `iInf_eq_bot` `tsub_eq_zero_of_le` `bot_eq_zero` `le_antisymm` `le_iInf` `tsub_le_tsub_left` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_iSup` `le_sub_of_add_le_left` `ne_top_of_le_ne_top` `iSup_le` `add_le_of_le_tsub_right_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `iInf_le_of_le` `tsub_le_self` `sub_sub_cancel` `iInf_le`

(root)

Definitions

Name	Category	Theorems
`instCompleteLinearOrderENat` 📖	CompOp	104 math math: `ENat.sub_iInf`, `ENat.sSup_eq_top_of_infinite`, `ENat.iInf_mul_of_ne`, `ENat.smul_sSup`, `ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime`, `ENat.iSup_add_iSup_of_monotone`, `ENat.iSup_zero`, `ENat.iInf_toNat`, `ENat.iInf_add_iInf`, `ENat.iInf_sum`, `Ideal.sup_primeHeight_eq_ringKrullDim`, `Submodule.spanRank_toENat_eq_iInf_encard`, `ENat.exists_eq_iSup_of_lt_top`, `ENat.mul_iSup`, `ENat.sSup_eq_zero`, `ENat.biSup_add'`, `ENat.sum_iSup`, `ENat.iInf_mul'`, `Order.krullDim_le_of_krullDim_preimage_le`, `ENat.iInf_coe_lt_top`, `ENat.iInf_mul`, `ENat.add_iInf`, `MvPowerSeries.le_order_subst`, `ENat.add_iSup`, `SimpleGraph.chromaticNumber_eq_iInf`, `ENat.mul_sSup`, `SimpleGraph.chromaticNumber_sum`, `Order.krullDim_eq_iSup_coheight_of_nonempty`, `ENat.coe_sSup`, `ENat.sInf_eq_zero`, `Order.krullDim_eq_iSup_length`, `Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim`, `ENat.sInf_add`, `ENat.add_sSup`, `Order.coheight_eq_iSup_head_eq`, `ENat.coe_iSup`, `ENat.smul_iSup`, `Order.krullDim_eq_iSup_height_of_nonempty`, `ENat.sub_iSup`, `ENat.iInf_eq_top_of_isEmpty`, `ENat.iInf_coe_eq_top`, `MvPowerSeries.le_weightedOrder_subst`, `ENat.exists_eq_iInf`, `Order.height_eq_iSup_lt_height`, `ENat.coe_iInf`, `ENat.mul_iInf_of_ne`, `ENat.iSup_natCast`, `ENat.iInf_add_iInf_of_monotone`, `Order.krullDim_eq_iSup_coheight`, `SimpleGraph.edist_eq_sInf`, `ENat.iSup_mul`, `le_analyticOrderAt_sub`, `le_analyticOrderAt_add`, `SimpleGraph.ediam_eq_iSup_iSup_edist`, `Order.krullDim_eq_iSup_height`, `ENat.sSup_add`, `Submodule.spanRank_toENat_eq_iInf_finset_card`, `ENat.coe_sInf`, `ENat.add_sInf`, `ENat.iSup_eq_zero`, `ENat.biSup_add_biSup_le'`, `ENat.iSup_add_iSup`, `ENat.iSup_add`, `ENat.le_iInf_add_iInf`, `Polynomial.ringKrullDim_le`, `ENat.mul_iInf`, `SimpleGraph.diam_def`, `ENat.sSup_mul`, `ENat.iSup_coe_eq_top`, `ENat.iInf_add`, `ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal`, `cauchy_davenport_minOrder_add`, `SimpleGraph.chromaticNumber_eq_biInf`, `Order.krullDim_eq_iSup_height_add_coheight_of_nonempty`, `SimpleGraph.ediam_def`, `Ideal.sup_height_eq_ringKrullDim`, `ENat.toENNReal_iSup`, `ENat.add_iInf₂`, `ENat.add_biSup`, `ENat.mul_iInf'`, `ENat.sum_iSup_of_monotone`, `ENat.iInf_eq_zero`, `Order.coheight_eq`, `cauchy_davenport_minOrder_mul`, `ENat.sSup_eq_zero'`, `ENat.le_iInf₂_add_iInf₂`, `ENat.biSup_add_biSup_le`, `Set.chainHeight_eq_iSup`, `ENat.exists_eq_iSup₂_of_lt_top`, `ENat.iSup_add_iSup_le`, `Order.height_eq_iSup_last_eq`, `ENat.toENNReal_iInf`, `Order.coheight_eq_iSup_gt_coheight`, `ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime`, `ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal`, `ENat.add_biSup'`, `ENat.biSup_add`, `ENat.iInf₂_add`, `Order.krullDim_le_of_krullDim_preimage_le'`, `SimpleGraph.eccent_def`, `ENat.iSup_coe_lt_top`, `analyticOrderAt_add_of_ne`, `ENat.sSup_mem_of_nonempty_of_lt_top`, `SimpleGraph.radius_eq_iInf_iSup_edist`
`instCompleteLinearOrderWithBotENat` 📖	CompOp	—

---

← Back to Index