Extended

📁 Source: Mathlib/Algebra/Order/Floor/Extended.lean

Statistics

Metric	Count
Definitions `ceil`, `floor`, `«term⌈_⌉ₑ»`, `«term⌊_⌋ₑ»`, `evalENatCeil`	5
Theorems `ceil_add_le`, `ceil_add_natCast`, `ceil_add_ofNat`, `ceil_add_one`, `ceil_add_toENNReal`, `ceil_coe`, `ceil_congr`, `ceil_eq_top`, `ceil_eq_zero`, `ceil_le`, `ceil_le_ceil`, `ceil_le_floor_add_one`, `ceil_lt`, `ceil_lt_add_one`, `ceil_lt_top`, `ceil_mono`, `ceil_natCast`, `ceil_natCast_add`, `ceil_ofNat`, `ceil_one`, `ceil_pos`, `ceil_sub_natCast`, `ceil_sub_ofNat`, `ceil_sub_one`, `ceil_sub_toENNReal`, `ceil_toENNReal_add`, `ceil_top`, `ceil_zero`, `floor_add_natCast`, `floor_add_ofNat`, `floor_add_one`, `floor_add_toENNReal`, `floor_coe`, `floor_congr`, `floor_eq_top`, `floor_eq_zero`, `floor_le`, `floor_le_ceil`, `floor_le_floor`, `floor_le_self`, `floor_lt`, `floor_lt_ceil`, `floor_lt_top`, `floor_mono`, `floor_natCast`, `floor_natCast_add`, `floor_ofNat`, `floor_one`, `floor_pos`, `floor_sub_natCast`, `floor_sub_ofNat`, `floor_sub_one`, `floor_sub_toENNReal`, `floor_toENNReal_add`, `floor_top`, `floor_zero`, `gc_ceil_toENNReal`, `gc_toENNReal_floor`, `le_ceil`, `le_ceil_self`, `le_floor`, `lt_ceil`, `lt_floor`, `toENNReal_iInf`, `toENNReal_iSup`, `natCeil_pos`	66
Total	71

ENat

Definitions

Name	Category	Theorems
`ceil` 📖	CompOp	35 math math: `ceil_eq_top`, `le_ceil_self`, `ceil_add_ofNat`, `ceil_top`, `ceil_le_ceil`, `ceil_add_natCast`, `ceil_sub_one`, `ceil_lt_add_one`, `floor_le_ceil`, `ceil_lt_top`, `ceil_le`, `ceil_lt`, `ceil_pos`, `ceil_add_le`, `lt_ceil`, `floor_lt_ceil`, `ceil_natCast_add`, `gc_ceil_toENNReal`, `ceil_sub_natCast`, `ceil_zero`, `ceil_add_toENNReal`, `le_ceil`, `ceil_sub_toENNReal`, `ceil_congr`, `ceil_mono`, `ceil_one`, `ceil_sub_ofNat`, `ceil_natCast`, `ceil_add_one`, `ceil_coe`, `ceil_toENNReal_add`, `ceil_le_floor_add_one`, `ceil_eq_zero`, `Mathlib.Meta.Positivity.natCeil_pos`, `ceil_ofNat`
`floor` 📖	CompOp	32 math math: `floor_pos`, `gc_toENNReal_floor`, `floor_add_ofNat`, `le_floor`, `floor_add_one`, `floor_add_natCast`, `floor_top`, `floor_le_ceil`, `floor_lt_ceil`, `floor_lt_top`, `floor_sub_natCast`, `floor_coe`, `floor_one`, `floor_mono`, `floor_sub_toENNReal`, `floor_le_self`, `floor_congr`, `floor_zero`, `floor_eq_top`, `floor_ofNat`, `floor_lt`, `floor_natCast_add`, `floor_sub_ofNat`, `floor_toENNReal_add`, `floor_add_toENNReal`, `floor_sub_one`, `lt_floor`, `floor_eq_zero`, `floor_le_floor`, `floor_natCast`, `ceil_le_floor_add_one`, `floor_le`
`«term⌈_⌉ₑ»` 📖	CompOp	—
`«term⌊_⌋ₑ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ceil_add_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instCommSemiringENat`	—	`top_add` `add_top` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Nat.ceil_add_le` `NNReal.instIsStrictOrderedRing`
`ceil_add_natCast` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `instNatCast`	—	`ceil_add_toENNReal`
`ceil_add_ofNat` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENat` `instCommSemiringENat`	—	`ceil_add_natCast`
`ceil_add_one` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.cast_one` `ceil_add_natCast`
`ceil_add_toENNReal` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `ENat` `instCommSemiringENat`	—	`top_add` `add_top` `ENNReal.ofNNReal_add_natCast` `Nat.ceil_add_natCast` `NNReal.instIsStrictOrderedRing` `zero_le'`
`ceil_coe` 📖	mathematical	—	`ceil` `ENNReal.ofNNReal` `ENat` `instNatCast` `Nat.ceil` `NNReal` `instSemiringNNReal` `instPartialOrderNNReal` `NNReal.instFloorSemiring`	—	—
`ceil_congr` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal`	`ceil`	—	`eq_of_forall_ge_iff`
`ceil_eq_top` 📖	mathematical	—	`ceil` `Top.top` `ENat` `instTopENat` `ENNReal` `instTopENNReal`	—	—
`ceil_eq_zero` 📖	mathematical	—	`ceil` `ENat` `instZeroENat` `ENNReal` `instZeroENNReal`	—	`toENNReal_zero` `ENNReal.instCanonicallyOrderedAdd` `ceil_le`
`ceil_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `ENNReal` `ENNReal.instPartialOrder` `toENNReal`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`ceil_le_ceil` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`ENat` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil`	—	`ceil_mono`
`ceil_le_floor_add_one` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `floor` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`le_rfl` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Nat.ceil_le_floor_add_one` `NNReal.instIsStrictOrderedRing`
`ceil_lt` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `ENNReal.instSub` `toENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Iff.not` `le_ceil`
`ceil_lt_add_one` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `ceil` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`CanLift.prf` `ENNReal.canLift` `Nat.cast_one` `Nat.ceil_lt_add_one` `NNReal.instIsStrictOrderedRing` `zero_le` `NNReal.instCanonicallyOrderedAdd`
`ceil_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `Top.top` `instTopENat` `ENNReal` `ENNReal.instPartialOrder` `instTopENNReal`	—	—
`ceil_mono` 📖	mathematical	—	`Monotone` `ENNReal` `ENat` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil`	—	`LE.le.trans` `le_ceil_self`
`ceil_natCast` 📖	mathematical	—	`ceil` `toENNReal`	—	`eq_of_forall_ge_iff`
`ceil_natCast_add` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `instNatCast`	—	`ceil_toENNReal_add`
`ceil_ofNat` 📖	mathematical	—	`ceil`	—	`ceil_natCast`
`ceil_one` 📖	mathematical	—	`ceil` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`toENNReal_one` `ceil_natCast`
`ceil_pos` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instZeroENat` `ceil` `ENNReal` `ENNReal.instPartialOrder` `instZeroENNReal`	—	`toENNReal_zero`
`ceil_sub_natCast` 📖	mathematical	—	`ceil` `ENNReal` `ENNReal.instSub` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instSubENat` `instNatCast`	—	`ceil_sub_toENNReal`
`ceil_sub_ofNat` 📖	mathematical	—	`ceil` `ENNReal` `ENNReal.instSub` `ENat` `instSubENat`	—	`ceil_sub_toENNReal`
`ceil_sub_one` 📖	mathematical	—	`ceil` `ENNReal` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instSubENat` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one` `toENNReal_one` `ceil_sub_toENNReal`
`ceil_sub_toENNReal` 📖	mathematical	—	`ceil` `ENNReal` `ENNReal.instSub` `toENNReal` `ENat` `instSubENat`	—	`tsub_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `ceil_zero` `ENNReal.top_sub` `ENNReal.sub_top` `sub_top` `ENNReal.ofNNReal_sub_natCast` `Nat.ceil_sub_natCast` `NNReal.instIsStrictOrderedRing` `NNReal.instOrderedSub` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd`
`ceil_toENNReal_add` 📖	mathematical	—	`ceil` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `ENat` `instCommSemiringENat`	—	`add_comm` `ceil_add_toENNReal`
`ceil_top` 📖	mathematical	—	`ceil` `Top.top` `ENNReal` `instTopENNReal` `ENat` `instTopENat`	—	—
`ceil_zero` 📖	mathematical	—	`ceil` `ENNReal` `instZeroENNReal` `ENat` `instZeroENat`	—	`toENNReal_zero` `ceil_natCast`
`floor_add_natCast` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `instNatCast`	—	`floor_add_toENNReal`
`floor_add_ofNat` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENat` `instCommSemiringENat`	—	`floor_add_natCast`
`floor_add_one` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Nat.cast_one` `floor_add_natCast`
`floor_add_toENNReal` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `ENat` `instCommSemiringENat`	—	`top_add` `add_top` `ENNReal.ofNNReal_add_natCast` `Nat.floor_add_natCast` `NNReal.instIsStrictOrderedRing` `zero_le'`
`floor_coe` 📖	mathematical	—	`floor` `ENNReal.ofNNReal` `ENat` `instNatCast` `Nat.floor` `NNReal` `instSemiringNNReal` `instPartialOrderNNReal` `NNReal.instFloorSemiring`	—	—
`floor_congr` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal`	`floor`	—	`eq_of_forall_le_iff`
`floor_eq_top` 📖	mathematical	—	`floor` `Top.top` `ENat` `instTopENat` `ENNReal` `instTopENNReal`	—	—
`floor_eq_zero` 📖	mathematical	—	`floor` `ENat` `instZeroENat` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`toENNReal_zero` `zero_add`
`floor_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ENNReal` `Preorder.toLT` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`lt_add_one_iff` `toENNReal_add` `toENNReal_one`
`floor_le_ceil` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ceil`	—	`LE.le.trans` `floor_le_self` `le_ceil_self`
`floor_le_floor` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`ENat` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor`	—	`floor_mono`
`floor_le_self` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `floor`	—	`le_floor` `le_rfl`
`floor_lt` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ENNReal` `ENNReal.instPartialOrder` `toENNReal`	—	`lt_iff_lt_of_le_iff_le` `le_floor`
`floor_lt_ceil` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`ENat` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ceil`	—	`floor_lt` `LT.lt.trans_le` `le_ceil_self`
`floor_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `Top.top` `instTopENat` `ENNReal` `ENNReal.instPartialOrder` `instTopENNReal`	—	—
`floor_mono` 📖	mathematical	—	`Monotone` `ENNReal` `ENat` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor`	—	`LE.le.trans'` `floor_le_self`
`floor_natCast` 📖	mathematical	—	`floor` `toENNReal`	—	`eq_of_forall_le_iff`
`floor_natCast_add` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instCommSemiringENat` `instNatCast`	—	`floor_toENNReal_add`
`floor_ofNat` 📖	mathematical	—	`floor`	—	`floor_natCast`
`floor_one` 📖	mathematical	—	`floor` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`toENNReal_one` `floor_natCast`
`floor_pos` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instZeroENat` `floor` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`toENNReal_zero` `zero_add`
`floor_sub_natCast` 📖	mathematical	—	`floor` `ENNReal` `ENNReal.instSub` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instSubENat` `instNatCast`	—	`floor_sub_toENNReal`
`floor_sub_ofNat` 📖	mathematical	—	`floor` `ENNReal` `ENNReal.instSub` `ENat` `instSubENat`	—	`floor_sub_toENNReal`
`floor_sub_one` 📖	mathematical	—	`floor` `ENNReal` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENat` `instSubENat` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.cast_one` `toENNReal_one` `floor_sub_toENNReal`
`floor_sub_toENNReal` 📖	mathematical	—	`floor` `ENNReal` `ENNReal.instSub` `toENNReal` `ENat` `instSubENat`	—	`tsub_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `floor_zero` `ENNReal.top_sub` `ENNReal.sub_top` `sub_top` `ENNReal.ofNNReal_sub_natCast` `Nat.floor_sub_natCast` `NNReal.instIsStrictOrderedRing` `NNReal.instOrderedSub` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd`
`floor_toENNReal_add` 📖	mathematical	—	`floor` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `ENat` `instCommSemiringENat`	—	`add_comm` `floor_add_toENNReal`
`floor_top` 📖	mathematical	—	`floor` `Top.top` `ENNReal` `instTopENNReal` `ENat` `instTopENat`	—	—
`floor_zero` 📖	mathematical	—	`floor` `ENNReal` `instZeroENNReal` `ENat` `instZeroENat`	—	`toENNReal_zero` `floor_natCast`
`gc_ceil_toENNReal` 📖	mathematical	—	`GaloisConnection` `ENNReal` `ENat` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `toENNReal`	—	`ceil_le`
`gc_toENNReal_floor` 📖	mathematical	—	`GaloisConnection` `ENat` `ENNReal` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ENNReal.instPartialOrder` `toENNReal` `floor`	—	`le_floor`
`le_ceil` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `ENNReal` `Preorder.toLT` `ENNReal.instPartialOrder` `ENNReal.instSub` `toENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`CanLift.prf` `canLift` `Nat.cast_one` `ENNReal.coe_lt_top` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.natCast_sub` `Nat.cast_tsub` `NNReal.instIsOrderedRing` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `ENNReal.coe_sub` `Nat.add_one_le_ceil_iff`
`le_ceil_self` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `ceil`	—	`ceil_le` `le_rfl`
`le_floor` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ENNReal` `ENNReal.instPartialOrder` `toENNReal`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `NNReal.instCanonicallyOrderedAdd`
`lt_ceil` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ceil` `ENNReal` `ENNReal.instPartialOrder` `toENNReal`	—	`lt_iff_lt_of_le_iff_le` `ceil_le`
`lt_floor` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `floor` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `toENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`add_one_le_iff` `toENNReal_add` `toENNReal_one`
`toENNReal_iInf` 📖	mathematical	—	`toENNReal` `iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ENNReal` `ENNReal.instCompleteLinearOrder`	—	`eq_of_forall_le_iff`
`toENNReal_iSup` 📖	mathematical	—	`toENNReal` `iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ENNReal` `ENNReal.instCompleteLinearOrder`	—	`eq_of_forall_ge_iff`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalENatCeil` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natCeil_pos` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	`ENat` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instZeroENat` `ENat.ceil`	—	`ENat.ceil_pos`

---

← Back to Index