ENatENNReal

📁 Source: Mathlib/Data/Real/ENatENNReal.lean

Statistics

Metric	Count
Definitions `hasCoeENNReal`, `toENNReal`, `toENNRealOrderEmbedding`, `toENNRealRingHom`	4
Theorems `map_coe_nnreal`, `toENNRealOrderEmbedding_apply`, `toENNRealRingHom_apply`, `toENNReal_add`, `toENNReal_coe`, `toENNReal_eq_top`, `toENNReal_inj`, `toENNReal_le`, `toENNReal_lt`, `toENNReal_lt_top`, `toENNReal_max`, `toENNReal_min`, `toENNReal_mono`, `toENNReal_mul`, `toENNReal_ne_top`, `toENNReal_ofNat`, `toENNReal_one`, `toENNReal_pow`, `toENNReal_strictMono`, `toENNReal_sub`, `toENNReal_top`, `toENNReal_zero`	22
Total	26

ENat

Definitions

Name	Category	Theorems
`hasCoeENNReal` 📖	CompOp	—
`toENNReal` 📖	CompOp	50 math math: `toENNReal_lt_top`, `ENNReal.tsum_set_const`, `le_ceil_self`, `gc_toENNReal_floor`, `toENNReal_strictMono`, `MeasureTheory.Measure.count_apply`, `le_floor`, `map_coe_nnreal`, `ceil_lt_add_one`, `toENNReal_sub`, `ENNReal.tsum_set_one`, `toENNReal_top`, `ceil_le`, `ceil_lt`, `lt_ceil`, `toENNRealRingHom_apply`, `toENNReal_zero`, `gc_ceil_toENNReal`, `toENNReal_lt`, `toENNReal_min`, `ceil_add_toENNReal`, `toENNReal_ofNat`, `toENNReal_mono`, `floor_sub_toENNReal`, `le_ceil`, `Dynamics.coverEntropyEntourage_le_log_coverMincard_div`, `floor_le_self`, `ceil_sub_toENNReal`, `toENNReal_eq_top`, `toENNReal_one`, `toENNReal_add`, `toENNReal_inj`, `MeasureTheory.Measure.count_univ`, `floor_lt`, `toENNReal_mul`, `toENNReal_max`, `toENNReal_pow`, `toENNReal_coe`, `floor_toENNReal_add`, `floor_add_toENNReal`, `toENNReal_iSup`, `lt_floor`, `ceil_natCast`, `toENNReal_le`, `ENNReal.tsum_const`, `ceil_toENNReal_add`, `toENNReal_iInf`, `floor_natCast`, `ENNReal.tsum_one`, `floor_le`
`toENNRealOrderEmbedding` 📖	CompOp	1 math math: `toENNRealOrderEmbedding_apply`
`toENNRealRingHom` 📖	CompOp	1 math math: `toENNRealRingHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_coe_nnreal` 📖	mathematical	—	`map` `NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `toENNReal`	—	—
`toENNRealOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `ENat` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENNReal.instPartialOrder` `RelEmbedding.instFunLike` `toENNRealOrderEmbedding` `WithTop.map` `NNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	—
`toENNRealRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ENat` `ENNReal` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENNReal.instCommSemiring` `RingHom.instFunLike` `toENNRealRingHom` `toENNReal`	—	—
`toENNReal_add` 📖	mathematical	—	`toENNReal` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENNReal` `ENNReal.instCommSemiring`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`toENNReal_coe` 📖	mathematical	—	`toENNReal` `ENat` `instNatCast` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	—
`toENNReal_eq_top` 📖	mathematical	—	`toENNReal` `Top.top` `ENNReal` `instTopENNReal` `ENat` `instTopENat`	—	—
`toENNReal_inj` 📖	mathematical	—	`toENNReal`	—	`OrderEmbedding.eq_iff_eq`
`toENNReal_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`OrderEmbedding.le_iff_le`
`toENNReal_lt` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`OrderEmbedding.lt_iff_lt`
`toENNReal_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `toENNReal` `Top.top` `instTopENNReal` `ENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instTopENat`	—	—
`toENNReal_max` 📖	mathematical	—	`toENNReal` `ENat` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENNReal` `ENNReal.instMax`	—	`Monotone.map_max` `toENNReal_mono`
`toENNReal_min` 📖	mathematical	—	`toENNReal` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENNReal` `ENNReal.instMin`	—	`Monotone.map_min` `toENNReal_mono`
`toENNReal_mono` 📖	mathematical	—	`Monotone` `ENat` `ENNReal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENNReal.instPartialOrder` `toENNReal`	—	`OrderEmbedding.monotone`
`toENNReal_mul` 📖	mathematical	—	`toENNReal` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENNReal` `ENNReal.instCommSemiring`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`toENNReal_ne_top` 📖	—	—	—	—	—
`toENNReal_ofNat` 📖	mathematical	—	`toENNReal`	—	—
`toENNReal_one` 📖	mathematical	—	`toENNReal` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENNReal` `instAddCommMonoidWithOneENNReal`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`toENNReal_pow` 📖	mathematical	—	`toENNReal` `ENat` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiringENat` `ENNReal` `ENNReal.instCommSemiring`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`toENNReal_strictMono` 📖	mathematical	—	`StrictMono` `ENat` `ENNReal` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENNReal.instPartialOrder` `toENNReal`	—	`OrderEmbedding.strictMono`
`toENNReal_sub` 📖	mathematical	—	`toENNReal` `ENat` `instSubENat` `ENNReal` `ENNReal.instSub`	—	`WithTop.map_sub` `Nat.cast_tsub` `NNReal.instIsOrderedRing` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `Nat.cast_zero`
`toENNReal_top` 📖	mathematical	—	`toENNReal` `Top.top` `ENat` `instTopENat` `ENNReal` `instTopENNReal`	—	—
`toENNReal_zero` 📖	mathematical	—	`toENNReal` `ENat` `instZeroENat` `ENNReal` `instZeroENNReal`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

---

← Back to Index