ERealExp

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean

Statistics

Metric	Count
Definitions `exp`	1
Theorems `exp_add`, `exp_bot`, `exp_coe`, `exp_eq_top_iff`, `exp_eq_zero_iff`, `exp_le_exp`, `exp_le_exp_iff`, `exp_le_one_iff`, `exp_lt_exp`, `exp_lt_exp_iff`, `exp_lt_one_iff`, `exp_lt_top_iff`, `exp_monotone`, `exp_neg`, `exp_strictMono`, `exp_top`, `exp_zero`, `one_le_exp_iff`, `one_lt_exp_iff`, `zero_lt_exp_iff`	20
Total	21

EReal

Definitions

Name	Category	Theorems
`exp` 📖	CompOp	43 math math: `exp_bot`, `one_lt_exp_iff`, `ExpGrowth.eventually_le_exp`, `exp_strictMono`, `measurable_exp`, `ExpGrowth.expGrowthInf_exp`, `ExpGrowth.expGrowthInf_le_iff`, `tendsto_exp_nhds_zero_nhds_one`, `one_le_exp_iff`, `exp_lt_exp_iff`, `exp_monotone`, `exp_coe`, `exp_lt_exp`, `exp_eq_top_iff`, `ENNReal.rpow_eq_exp_mul_log`, `ExpGrowth.expGrowthSup_exp`, `tendsto_exp_nhds_top_nhds_top`, `ENNReal.exp_log`, `exp_le_one_iff`, `zero_lt_exp_iff`, `tendsto_exp_nhds_bot_nhds_zero`, `ExpGrowth.le_expGrowthInf_iff`, `ExpGrowth.frequently_le_exp`, `ENNReal.continuous_exp`, `ExpGrowth.frequently_exp_le`, `ExpGrowth.eventually_exp_le`, `exp_zero`, `exp_mul`, `exp_lt_one_iff`, `exp_nmul`, `exp_lt_top_iff`, `expOrderIso_apply`, `exp_add`, `ExpGrowth.expGrowthSup_le_iff`, `exp_eq_zero_iff`, `expHomeomorph_apply`, `ExpGrowth.le_expGrowthSup_iff`, `exp_le_exp_iff`, `exp_le_exp`, `exp_neg`, `log_exp`, `exp_top`, `Measurable.ereal_exp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_add` 📖	mathematical	—	`exp` `EReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`bot_add` `MulZeroClass.zero_mul` `add_bot` `MulZeroClass.mul_zero` `ENNReal.ofReal_mul` `Real.exp_nonneg` `Real.exp_add` `ENNReal.mul_top` `ENNReal.top_mul` `add_top_of_ne_bot`
`exp_bot` 📖	mathematical	—	`exp` `Bot.bot` `EReal` `instBotEReal` `ENNReal` `instZeroENNReal`	—	—
`exp_coe` 📖	mathematical	—	`exp` `Real.toEReal` `ENNReal.ofReal` `Real.exp`	—	—
`exp_eq_top_iff` 📖	mathematical	—	`exp` `Top.top` `ENNReal` `instTopENNReal` `EReal` `instTop`	—	—
`exp_eq_zero_iff` 📖	mathematical	—	`exp` `ENNReal` `instZeroENNReal` `Bot.bot` `EReal` `instBotEReal`	—	—
`exp_le_exp` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal`	`ENNReal` `ENNReal.instPartialOrder` `exp`	—	—
`exp_le_exp_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `exp` `EReal` `instPartialOrderEReal`	—	`StrictMono.le_iff_le` `exp_strictMono`
`exp_le_one_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `exp` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EReal` `instPartialOrderEReal` `instZeroEReal`	—	`exp_le_exp_iff` `exp_zero`
`exp_lt_exp` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal`	`ENNReal` `ENNReal.instPartialOrder` `exp`	—	—
`exp_lt_exp_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `exp` `EReal` `instPartialOrderEReal`	—	`StrictMono.lt_iff_lt` `exp_strictMono`
`exp_lt_one_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `exp` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EReal` `instPartialOrderEReal` `instZeroEReal`	—	`exp_lt_exp_iff` `exp_zero`
`exp_lt_top_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `exp` `Top.top` `instTopENNReal` `EReal` `instPartialOrderEReal` `instTop`	—	`exp_lt_exp_iff` `exp_top`
`exp_monotone` 📖	mathematical	—	`Monotone` `EReal` `ENNReal` `PartialOrder.toPreorder` `instPartialOrderEReal` `ENNReal.instPartialOrder` `exp`	—	`StrictMono.monotone` `exp_strictMono`
`exp_neg` 📖	mathematical	—	`exp` `EReal` `instNeg` `ENNReal` `ENNReal.instInv`	—	`ENNReal.inv_zero` `exp_coe` `coe_neg` `ENNReal.ofReal_inv_of_pos` `Real.exp_pos` `Real.exp_neg` `ENNReal.inv_top`
`exp_strictMono` 📖	mathematical	—	`StrictMono` `EReal` `ENNReal` `PartialOrder.toPreorder` `instPartialOrderEReal` `ENNReal.instPartialOrder` `exp`	—	`exp_bot` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `exp_eq_zero_iff` `LT.lt.ne'` `ENNReal.ofReal_lt_ofReal_iff'` `Real.exp_strictMono` `Real.exp_pos` `not_top_lt`
`exp_top` 📖	mathematical	—	`exp` `Top.top` `EReal` `instTop` `ENNReal` `instTopENNReal`	—	—
`exp_zero` 📖	mathematical	—	`exp` `EReal` `instZeroEReal` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Real.exp_zero` `ENNReal.ofReal_one`
`one_le_exp_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `exp` `EReal` `instPartialOrderEReal` `instZeroEReal`	—	`exp_le_exp_iff` `exp_zero`
`one_lt_exp_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `exp` `EReal` `instPartialOrderEReal` `instZeroEReal`	—	`exp_lt_exp_iff` `exp_zero`
`zero_lt_exp_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `exp` `EReal` `instPartialOrderEReal` `Bot.bot` `instBotEReal`	—	`exp_lt_exp_iff` `exp_bot`

---

← Back to Index