Basic

📁 Source: Mathlib/Data/EReal/Basic.lean

Statistics

Metric	Count
Definitions toEReal, EReal, decidableLT, hasCoeENNReal, instCoeReal, instInhabited, instMul, instMulZeroOneClass, instTop, mul, neTopBotEquivReal, rec, toENNReal, toReal, evalENNRealToEReal, evalERealToENNReal, evalERealToReal, evalRealToEReal, toEReal, instAddCommMonoidEReal, instAddCommMonoidWithOneEReal, instAddMonoidEReal, instBotEReal, instCompleteLinearOrderEReal, instInfSetEReal, instLinearOrderEReal, instNontrivialEReal, instOneEReal, instPartialOrderEReal, instSupSetEReal, instZeroEReal	31
Theorems bot_lt_coe, bot_lt_coe_ennreal, bot_lt_zero, bot_ne_coe, bot_ne_zero, canLift, coe_add, coe_coe_eq_natCast, coe_ennreal_add, coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_eq_one, coe_ennreal_eq_top_iff, coe_ennreal_eq_zero, coe_ennreal_injective, coe_ennreal_le_coe_ennreal_iff, coe_ennreal_lt_coe_ennreal_iff, coe_ennreal_mul, coe_ennreal_ne_bot, coe_ennreal_ne_coe_ennreal_iff, coe_ennreal_ne_one, coe_ennreal_ne_zero, coe_ennreal_nonneg, coe_ennreal_nsmul, coe_ennreal_ofReal, coe_ennreal_one, coe_ennreal_pos, coe_ennreal_pos_iff_ne_zero, coe_ennreal_strictMono, coe_ennreal_toReal, coe_ennreal_top, coe_ennreal_zero, coe_eq_coe_iff, coe_eq_one, coe_eq_zero, coe_injective, coe_le_coe, coe_le_coe_iff, coe_lt_coe, coe_lt_coe_iff, coe_lt_top, coe_mul, coe_natCast, coe_ne_bot, coe_ne_coe_iff, coe_ne_one, coe_ne_top, coe_ne_zero, coe_neg', coe_nnreal_eq_coe_real, coe_nnreal_lt_top, coe_nnreal_ne_top, coe_nonneg, coe_nonpos, coe_nsmul, coe_one, coe_pos, coe_strictMono, coe_toENNReal, coe_toENNReal_eq_max, coe_toReal, coe_toReal_le, coe_zero, eq_bot_iff_forall_lt, eq_top_iff_forall_lt, exists, exists_between_coe_real, exists_rat_btwn_of_lt, forall, image_coe_Icc, image_coe_Ici, image_coe_Ico, image_coe_Iic, image_coe_Iio, image_coe_Ioc, image_coe_Ioi, image_coe_Ioo, induction₂, induction₂_symm, instCanLiftENNRealToERealLeOfNat, le_coe_toReal, lt_iff_exists_rat_btwn, lt_iff_exists_real_btwn, mul_comm, natCast_eq_iff, natCast_le_iff, natCast_lt_iff, natCast_mul, natCast_ne_bot, natCast_ne_iff, natCast_ne_top, one_mul, preimage_coe_Icc, preimage_coe_Ici, preimage_coe_Ico, preimage_coe_Ico_top, preimage_coe_Iic, preimage_coe_Iio, preimage_coe_Iio_top, preimage_coe_Ioc, preimage_coe_Ioc_bot, preimage_coe_Ioi, preimage_coe_Ioi_bot, preimage_coe_Ioo, preimage_coe_Ioo_bot, preimage_coe_Ioo_bot_top, preimage_coe_Ioo_top, range_coe, range_coe_ennreal, range_coe_eq_Ioo, real_coe_toENNReal, toENNReal_bot, toENNReal_coe, toENNReal_eq_toENNReal, toENNReal_eq_top_iff, toENNReal_eq_zero_iff, toENNReal_le_toENNReal, toENNReal_lt_toENNReal, toENNReal_ne_top_iff, toENNReal_ne_zero_iff, toENNReal_of_ne_top, toENNReal_of_nonpos, toENNReal_pos_iff, toENNReal_top, toENNReal_zero, toReal_bot, toReal_coe, toReal_coe_ennreal, toReal_eq_toReal, toReal_eq_zero_iff, toReal_image_Ioo_bot_zero, toReal_image_Ioo_zero_top, toReal_le_toReal, toReal_ne_zero_iff, toReal_neg, toReal_nonneg, toReal_nonpos, toReal_one, toReal_pos, toReal_toENNReal, toReal_top, toReal_zero, top_ne_coe, top_ne_zero, zero_lt_top, zero_mul, zero_ne_bot, zero_ne_top, instCharZeroEReal, instDenselyOrderedEReal, instIsOrderedAddMonoidEReal, instZeroLEOneClassEReal	151
Total	182

ENNReal

Definitions

Name	Category	Theorems
toEReal 📖	CompOp	47 math math: EReal.coe_ennreal_add, EReal.coe_ennreal_le_coe_ennreal_iff, EReal.coe_ennreal_pow, EReal.coe_ennreal_mul_top, EReal.top_mul_coe_ennreal, EReal.isClosedEmbedding_coe_ennreal, EReal.abs_mul_sign, EReal.range_coe_ennreal, EReal.coe_ennreal_eq_coe_ennreal_iff, EReal.recENNReal_coe_ennreal, EReal.instCanLiftENNRealToERealLeOfNat, Measurable.coe_ereal_ennreal, EReal.coe_ennreal_zero, EReal.tendsto_coe_ennreal, EReal.toReal_coe_ennreal, continuous_coe_ennreal_ereal, EReal.coe_toENNReal_eq_max, EReal.coe_ennreal_eq_zero, measurable_coe_ennreal_ereal, EReal.bot_lt_coe_ennreal, EReal.coe_ennreal_eq_one, EReal.coe_ennreal_lt_coe_ennreal_iff, EReal.coe_ennreal_toReal, EReal.isEmbedding_coe_ennreal, toEReal_sub, AEMeasurable.coe_ereal_ennreal, EReal.coe_ennreal_injective, EReal.coe_nnreal_eq_coe_real, EReal.sign_mul_inv_abs, EReal.coe_ennreal_strictMono, EReal.sign_mul_abs, EReal.coe_toENNReal, EReal.coe_ennreal_one, EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal, EReal.coe_abs, EReal.continuous_coe_ennreal_iff, EReal.toENNReal_coe, EReal.coe_ennreal_nsmul, EReal.coe_ennreal_nonneg, EReal.coe_nnreal_lt_top, EReal.coe_ennreal_ofReal, EReal.coe_ennreal_pos_iff_ne_zero, EReal.coe_ennreal_mul, EReal.sign_mul_inv_abs', EReal.coe_ennreal_eq_top_iff, EReal.coe_ennreal_top, EReal.coe_ennreal_pos

EReal

Definitions

Name	Category	Theorems
decidableLT 📖	CompOp	11 math math: sign_eq_and_abs_eq_iff_eq, abs_mul_sign, sign_mul, sign_coe, sign_bot, sign_top, le_iff_sign, sign_mul_inv_abs, sign_mul_abs, sign_neg, sign_mul_inv_abs'
hasCoeENNReal 📖	CompOp	—
instCoeReal 📖	CompOp	—
instInhabited 📖	CompOp	—
instMul 📖	CompOp	125 math math: toENNReal_mul', bot_mul_coe_of_neg, natCast_mul, div_eq_inv_mul, ExpGrowth.eventually_le_exp, mul_nonneg, instMeasurableMul₂, mul_nonpos_iff, bot_mul_coe_of_pos, Tendsto.mul, ExpGrowth.expGrowthInf_exp, Monotone.expGrowthInf_comp_mul, div_mul_div_comm, left_distrib_of_nonneg, ExpGrowth.expGrowthInf_le_iff, instPosMulMono, coe_ennreal_mul_top, top_mul_coe_of_pos, top_mul_coe_ennreal, LinearGrowth.frequently_mul_le, top_mul_of_pos, Monotone.expGrowthInf_comp, exists_nat_ge_mul, abs_mul_sign, mul_div_mul_cancel, instMulPosMono, LinearGrowth.linearGrowthInf_const_mul_self, one_mul, lt_div_iff, right_distrib_of_nonneg_of_ne_top, mul_top_of_neg, sign_mul, bot_mul_bot, Tendsto.mul_const, mul_div, nsmul_eq_mul, LinearGrowth.linearGrowthSup_le_iff, ExpGrowth.le_expGrowthInf_comp, LinearGrowth.linearGrowthSup_const_mul_self, mul_nonneg_iff, abs_mul, mul_top_of_pos, ENNReal.rpow_eq_exp_mul_log, mul_neg_iff, ExpGrowth.expGrowthSup_exp, coe_mul_top_of_pos, le_limsup_mul, limsup_mul_le, le_liminf_mul, ENNReal.log_pow, toENNReal_mul, ExpGrowth.le_expGrowthInf_iff, ExpGrowth.expGrowthSup_comp_le, Tendsto.const_mul, bot_mul_top, ExpGrowth.frequently_le_exp, liminf_mul_le, ExpGrowth.frequently_exp_le, top_mul_bot, Monotone.expGrowthInf_comp_le, instNoZeroDivisors, bot_mul_of_pos, div_lt_iff, LinearGrowth.eventually_mul_le, ENNReal.log_rpow, mul_comm, LinearGrowth.frequently_le_mul, mul_pos, ExpGrowth.eventually_exp_le, instMulPosReflectLT, mul_div_cancel, mul_bot_of_pos, mul_eq_bot, toReal_mul, mul_le_mul_of_nonpos_right, top_mul_of_neg, exp_mul, LinearGrowth.le_linearGrowthInf_iff, coe_mul, LinearGrowth.linearGrowthInf_le_iff, left_distrib_of_nonneg_of_ne_top, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, top_mul_top, mul_div_left_comm, Monotone.linearGrowthInf_comp_mul, exp_nmul, LinearGrowth.eventually_le_mul, coe_mul_bot_of_neg, sign_mul_inv_abs, div_mul_cancel, ExpGrowth.expGrowthSup_le_iff, sign_mul_abs, Monotone.linearGrowthInf_comp, mul_div_right, tendsto_mul, mul_pos_iff, coe_mul_bot_of_pos, right_distrib_of_nonneg, mul_inv, Monotone.linearGrowthSup_comp_mul, Monotone.le_linearGrowthSup_comp, div_le_iff_le_mul, div_eq_iff, mul_bot_of_neg, bot_mul_of_neg, zero_mul, Monotone.expGrowthSup_comp, Monotone.linearGrowthSup_comp, neg_mul, Monotone.expGrowthSup_comp_mul, coe_ennreal_mul, continuousAt_mul, LinearGrowth.le_linearGrowthInf_comp, mul_eq_top, LinearGrowth.le_linearGrowthSup_iff, ExpGrowth.le_expGrowthSup_iff, le_div_iff_mul_le, sign_mul_inv_abs', div_div, coe_mul_top_of_neg, instPosMulReflectLT, LinearGrowth.EReal.eventually_atTop_exists_nat_between, top_mul_coe_of_neg, Monotone.le_expGrowthSup_comp
instMulZeroOneClass 📖	CompOp	—
instTop 📖	CompOp	98 math math: nhds_top_basis, LinearGrowth.linearGrowthSup_top, continuousAt_add_coe_top, bot_mul_coe_of_neg, sub_top, toENNReal_top, LSeries_injOn, LSeries_eventually_eq_zero_iff', forall, top_div_of_neg_ne_bot, top_sub, neg_eq_top_iff, coe_ennreal_mul_top, top_mul_coe_of_pos, add_lt_top, top_mul_coe_ennreal, tendsto_coe_atTop, ENNReal.log_top, bot_div_of_neg_ne_bot, top_mul_of_pos, nhds_top', canLift, LinearGrowth.linearGrowthInf_top, preimage_coe_Ioo_top, tendsto_toReal_atTop, top_add_of_ne_bot, top_sub_bot, range_coe_eq_Ioo, abs_top, toENNReal_eq_top_iff, mul_top_of_neg, bot_mul_bot, top_sub_coe, range_coe, top_add_iff_ne_bot, continuousOn_toReal, exp_eq_top_iff, mul_top_of_pos, LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos, tendsto_exp_nhds_top_nhds_top, image_coe_Ici, toReal_top, Dynamics.coverEntropyEntourage_finite_of_isCompact_invariant, add_top_of_ne_bot, coe_mul_top_of_pos, top_add_coe, neg_eq_bot_iff, ENNReal.log_lt_top_iff, bot_mul_top, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, coe_add_top, preimage_coe_Ico_top, exists, inv_top, top_mul_bot, sub_bot, top_div_of_pos_ne_top, continuousAt_add_top_coe, sign_top, ENNReal.log_eq_top_iff, preimage_coe_Ioo_bot_top, tendsto_coe_nhds_top_iff, div_top, mul_eq_bot, top_mul_of_neg, preimage_coe_Iio_top, tendsto_nhds_top_iff_real, toReal_image_Ioo_zero_top, inv_lt_top, top_mul_top, ExpGrowth.expGrowthSup_top, coe_mul_bot_of_neg, exp_lt_top_iff, continuousAt_add_top_top, toReal_eq_zero_iff, ExpGrowth.expGrowthInf_top, nhds_top, coe_sub_bot, top_add_top, mul_bot_of_neg, bot_mul_of_neg, zero_lt_top, add_top_iff_ne_bot, coe_nnreal_lt_top, nhdsWithin_top, image_coe_Ioi, mul_eq_top, LSeries_eq_zero_iff, eq_top_iff_forall_lt, neg_top, coe_ennreal_eq_top_iff, coe_mul_top_of_neg, coe_ennreal_top, neg_bot, exp_top, mem_nhds_top_iff, coe_lt_top, top_mul_coe_of_neg
mul 📖	CompOp	—
neTopBotEquivReal 📖	CompOp	—
rec 📖	CompOp	—
toENNReal 📖	CompOp	29 math math: toENNReal_mul', real_coe_toENNReal, ContinuousWithinAt.ereal_toENNReal, toENNReal_lt_toENNReal, toENNReal_eq_zero_iff, toENNReal_top, toENNReal_le_toENNReal, measurable_ereal_toENNReal, toENNReal_pos_iff, toENNReal_of_ne_top, ContinuousOn.ereal_toENNReal, toENNReal_eq_top_iff, toENNReal_eq_toENNReal, toENNReal_sub, coe_toENNReal_eq_max, ContinuousAt.ereal_toENNReal, toENNReal_mul, AEMeasurable.ereal_toENNReal, toENNReal_zero, continuous_toENNReal, toENNReal_bot, toENNReal_add, toReal_toENNReal, coe_toENNReal, Continuous.ereal_toENNReal, toENNReal_coe, toENNReal_of_nonpos, toENNReal_add_le, Measurable.ereal_toENNReal
toReal 📖	CompOp	33 math math: Measurable.ereal_toReal, toENNReal_of_ne_top, measurable_ereal_toReal, le_coe_toReal, toReal_nonpos, toReal_zero, tendsto_toReal_atTop, tendsto_toReal_atBot, toReal_neg, continuousOn_toReal, toReal_coe_ennreal, toReal_neg_eq, toReal_top, coe_toReal, toReal_add, toReal_image_Ioo_bot_zero, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, toReal_bot, toReal_coe, AEMeasurable.ereal_toReal, toReal_mul, toReal_le_toReal, toReal_one, toReal_image_Ioo_zero_top, tendsto_toReal, toReal_toENNReal, toReal_eq_zero_iff, toReal_sub, toReal_pos, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, toReal_eq_toReal, coe_toReal_le, toReal_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_coe 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Real.toEReal	—	WithBot.bot_lt_coe
bot_lt_coe_ennreal 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal ENNReal.toEReal	—	LT.lt.trans_le bot_lt_coe coe_ennreal_nonneg
bot_lt_zero 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal instZeroEReal	—	bot_lt_coe
bot_ne_coe 📖	—	—	—	—	LT.lt.ne bot_lt_coe
bot_ne_zero 📖	—	—	—	—	coe_ne_bot
canLift 📖	mathematical	—	CanLift EReal Real Real.toEReal Top.top instTop Bot.bot instBotEReal	—	—
coe_add 📖	mathematical	—	Real.toEReal Real Real.instAdd EReal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal	—	—
coe_coe_eq_natCast 📖	mathematical	—	Real.toEReal Real Real.instNatCast EReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	—
coe_ennreal_add 📖	mathematical	—	ENNReal.toEReal ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EReal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal	—	—
coe_ennreal_eq_coe_ennreal_iff 📖	mathematical	—	ENNReal.toEReal	—	coe_ennreal_injective
coe_ennreal_eq_one 📖	mathematical	—	ENNReal.toEReal EReal instOneEReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	coe_ennreal_eq_coe_ennreal_iff coe_ennreal_one
coe_ennreal_eq_top_iff 📖	mathematical	—	ENNReal.toEReal Top.top EReal instTop ENNReal instTopENNReal	—	coe_ennreal_injective
coe_ennreal_eq_zero 📖	mathematical	—	ENNReal.toEReal EReal instZeroEReal ENNReal instZeroENNReal	—	coe_ennreal_eq_coe_ennreal_iff coe_ennreal_zero
coe_ennreal_injective 📖	mathematical	—	ENNReal EReal ENNReal.toEReal	—	StrictMono.injective coe_ennreal_strictMono
coe_ennreal_le_coe_ennreal_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal ENNReal.toEReal ENNReal ENNReal.instPartialOrder	—	StrictMono.le_iff_le coe_ennreal_strictMono
coe_ennreal_lt_coe_ennreal_iff 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal ENNReal.toEReal ENNReal ENNReal.instPartialOrder	—	StrictMono.lt_iff_lt coe_ennreal_strictMono
coe_ennreal_mul 📖	mathematical	—	ENNReal.toEReal ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EReal instMul	—	mul_comm mul_comm coe_ennreal_top
coe_ennreal_ne_bot 📖	—	—	—	—	LT.lt.ne' bot_lt_coe_ennreal
coe_ennreal_ne_coe_ennreal_iff 📖	—	—	—	—	coe_ennreal_injective
coe_ennreal_ne_one 📖	—	—	—	—	Iff.not coe_ennreal_eq_one
coe_ennreal_ne_zero 📖	—	—	—	—	Iff.not coe_ennreal_eq_zero
coe_ennreal_nonneg 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal ENNReal.toEReal	—	coe_ennreal_le_coe_ennreal_iff zero_le ENNReal.instCanonicallyOrderedAdd
coe_ennreal_nsmul 📖	mathematical	—	ENNReal.toEReal ENNReal AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EReal instAddMonoidEReal	—	map_nsmul AddMonoidHom.instAddMonoidHomClass coe_ennreal_zero coe_ennreal_add
coe_ennreal_ofReal 📖	mathematical	—	ENNReal.toEReal ENNReal.ofReal Real.toEReal Real Real.instMax Real.instZero	—	—
coe_ennreal_one 📖	mathematical	—	ENNReal.toEReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal EReal instOneEReal	—	—
coe_ennreal_pos 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal ENNReal.toEReal ENNReal ENNReal.instPartialOrder instZeroENNReal	—	coe_ennreal_zero coe_ennreal_lt_coe_ennreal_iff
coe_ennreal_pos_iff_ne_zero 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal ENNReal.toEReal	—	coe_ennreal_pos pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd
coe_ennreal_strictMono 📖	mathematical	—	StrictMono ENNReal EReal PartialOrder.toPreorder ENNReal.instPartialOrder instPartialOrderEReal ENNReal.toEReal	—	WithTop.strictMono_iff coe_lt_coe_iff coe_lt_top
coe_ennreal_toReal 📖	mathematical	—	Real.toEReal ENNReal.toReal ENNReal.toEReal	—	CanLift.prf ENNReal.canLift
coe_ennreal_top 📖	mathematical	—	ENNReal.toEReal Top.top ENNReal instTopENNReal EReal instTop	—	—
coe_ennreal_zero 📖	mathematical	—	ENNReal.toEReal ENNReal instZeroENNReal EReal instZeroEReal	—	—
coe_eq_coe_iff 📖	mathematical	—	Real.toEReal	—	coe_injective
coe_eq_one 📖	mathematical	—	Real.toEReal EReal instOneEReal Real Real.instOne	—	coe_eq_coe_iff
coe_eq_zero 📖	mathematical	—	Real.toEReal EReal instZeroEReal Real Real.instZero	—	coe_eq_coe_iff
coe_injective 📖	mathematical	—	Real EReal Real.toEReal	—	StrictMono.injective coe_strictMono
coe_le_coe 📖	mathematical	Real Real.instLE	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	coe_le_coe_iff
coe_le_coe_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Real.toEReal Real Real.instLE	—	StrictMono.le_iff_le coe_strictMono
coe_lt_coe 📖	mathematical	Real Real.instLT	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	coe_lt_coe_iff
coe_lt_coe_iff 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal Real Real.instLT	—	StrictMono.lt_iff_lt coe_strictMono
coe_lt_top 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal Top.top instTop	—	WithBot.coe_lt_coe WithTop.coe_lt_top
coe_mul 📖	mathematical	—	Real.toEReal Real Real.instMul EReal instMul	—	—
coe_natCast 📖	mathematical	—	Real.toEReal Real Real.instNatCast EReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	—
coe_ne_bot 📖	—	—	—	—	LT.lt.ne' bot_lt_coe
coe_ne_coe_iff 📖	—	—	—	—	coe_injective
coe_ne_one 📖	—	—	—	—	coe_ne_coe_iff
coe_ne_top 📖	—	—	—	—	LT.lt.ne coe_lt_top
coe_ne_zero 📖	—	—	—	—	coe_ne_coe_iff
coe_neg' 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal instZeroEReal Real Real.instLT Real.instZero	—	coe_lt_coe_iff
coe_nnreal_eq_coe_real 📖	mathematical	—	ENNReal.toEReal ENNReal.ofNNReal Real.toEReal NNReal.toReal	—	—
coe_nnreal_lt_top 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal ENNReal.toEReal ENNReal.ofNNReal Top.top instTop	—	coe_lt_top
coe_nnreal_ne_top 📖	—	—	—	—	coe_ne_top
coe_nonneg 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal Real.toEReal Real Real.instLE Real.instZero	—	coe_le_coe_iff
coe_nonpos 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Real.toEReal instZeroEReal Real Real.instLE Real.instZero	—	coe_le_coe_iff
coe_nsmul 📖	mathematical	—	Real.toEReal Real AddMonoid.toNatSMul Real.instAddMonoid EReal instAddMonoidEReal	—	map_nsmul AddMonoidHom.instAddMonoidHomClass coe_zero coe_add
coe_one 📖	mathematical	—	Real.toEReal Real Real.instOne EReal instOneEReal	—	—
coe_pos 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal Real.toEReal Real Real.instLT Real.instZero	—	coe_lt_coe_iff
coe_strictMono 📖	mathematical	—	StrictMono Real EReal Real.instPreorder PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	StrictMono.comp WithBot.coe_strictMono WithTop.coe_strictMono
coe_toENNReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	ENNReal.toEReal toENNReal	—	toENNReal.eq_1 max_eq_left coe_toReal
coe_toENNReal_eq_max 📖	mathematical	—	ENNReal.toEReal toENNReal EReal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal instZeroEReal	—	le_total coe_toENNReal max_eq_right toENNReal_of_nonpos max_eq_left coe_ennreal_zero
coe_toReal 📖	mathematical	—	Real.toEReal toReal	—	CanLift.prf canLift
coe_toReal_le 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Real.toEReal toReal	—	coe_toReal
coe_zero 📖	mathematical	—	Real.toEReal Real Real.instZero EReal instZeroEReal	—	—
eq_bot_iff_forall_lt 📖	mathematical	—	Bot.bot EReal instBotEReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	bot_lt_coe Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq coe_toReal_le
eq_top_iff_forall_lt 📖	mathematical	—	Top.top EReal instTop Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	coe_lt_top Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq le_coe_toReal
exists 📖	mathematical	—	Bot.bot EReal instBotEReal Top.top instTop Real.toEReal	—	—
exists_between_coe_real 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal	Real.toEReal	—	exists_between instDenselyOrderedEReal not_lt_bot not_top_lt
exists_rat_btwn_of_lt 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal	Real.toEReal Real Real.instRatCast	—	not_top_lt lt_irrefl LT.lt.trans bot_lt_coe exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean coe_lt_coe_iff exists_rat_gt coe_lt_top exists_rat_lt
forall 📖	mathematical	—	Bot.bot EReal instBotEReal Top.top instTop Real.toEReal	—	—
image_coe_Icc 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Icc Real.instPreorder PartialOrder.toPreorder instPartialOrderEReal	—	Set.image_comp WithTop.image_coe_Icc WithBot.image_coe_Icc
image_coe_Ici 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Ici Real.instPreorder Set.Ico PartialOrder.toPreorder instPartialOrderEReal Top.top instTop	—	Set.image_comp WithTop.image_coe_Ici WithBot.image_coe_Ico
image_coe_Ico 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Ico Real.instPreorder PartialOrder.toPreorder instPartialOrderEReal	—	Set.image_comp WithTop.image_coe_Ico WithBot.image_coe_Ico
image_coe_Iic 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Iic Real.instPreorder Set.Ioc PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal	—	Set.image_comp WithTop.image_coe_Iic WithBot.image_coe_Iic
image_coe_Iio 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Iio Real.instPreorder Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal	—	Set.image_comp WithTop.image_coe_Iio WithBot.image_coe_Iio
image_coe_Ioc 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Ioc Real.instPreorder PartialOrder.toPreorder instPartialOrderEReal	—	Set.image_comp WithTop.image_coe_Ioc WithBot.image_coe_Ioc
image_coe_Ioi 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Ioi Real.instPreorder Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Top.top instTop	—	Set.image_comp WithTop.image_coe_Ioi WithBot.image_coe_Ioo
image_coe_Ioo 📖	mathematical	—	Set.image Real EReal Real.toEReal Set.Ioo Real.instPreorder PartialOrder.toPreorder instPartialOrderEReal	—	Set.image_comp WithTop.image_coe_Ioo WithBot.image_coe_Ioo
induction₂ 📖	—	Top.top EReal instTop Real.toEReal instZeroEReal Bot.bot instBotEReal	—	—	lt_trichotomy
induction₂_symm 📖	—	Top.top EReal instTop Real.toEReal instZeroEReal Bot.bot instBotEReal	—	—	induction₂
instCanLiftENNRealToERealLeOfNat 📖	mathematical	—	CanLift EReal ENNReal ENNReal.toEReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	—	Eq.ge range_coe_ennreal
le_coe_toReal 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal Real.toEReal toReal	—	coe_toReal
lt_iff_exists_rat_btwn 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal Real Real.instRatCast	—	exists_rat_btwn_of_lt LT.lt.trans
lt_iff_exists_real_btwn 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal Real.toEReal	—	exists_rat_btwn_of_lt LT.lt.trans
mul_comm 📖	mathematical	—	EReal instMul	—	coe_mul mul_comm
natCast_eq_iff 📖	mathematical	—	EReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	coe_coe_eq_natCast coe_eq_coe_iff IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
natCast_le_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	coe_coe_eq_natCast coe_le_coe_iff Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
natCast_lt_iff 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	coe_coe_eq_natCast coe_lt_coe_iff Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
natCast_mul 📖	mathematical	—	EReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal instMul	—	coe_coe_eq_natCast Nat.cast_mul coe_mul
natCast_ne_bot 📖	—	—	—	—	instLawfulBCmpCompare_mathlib
natCast_ne_iff 📖	—	—	—	—	not_iff_not natCast_eq_iff
natCast_ne_top 📖	—	—	—	—	instLawfulBCmpCompare_mathlib
one_mul 📖	mathematical	—	EReal instMul instOneEReal	—	one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing one_mul
preimage_coe_Icc 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Icc PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	preimage_coe_Ici preimage_coe_Iic
preimage_coe_Ici 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ici PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	Set.preimage_comp WithBot.preimage_coe_Ici WithTop.preimage_coe_Ici
preimage_coe_Ico 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ico PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	preimage_coe_Ici preimage_coe_Iio
preimage_coe_Ico_top 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ico PartialOrder.toPreorder instPartialOrderEReal Top.top instTop Set.Ici Real.instPreorder	—	Set.Ici_inter_Iio preimage_coe_Ici preimage_coe_Iio_top Set.inter_univ
preimage_coe_Iic 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Iic PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	Set.preimage_comp WithBot.preimage_coe_Iic WithTop.preimage_coe_Iic
preimage_coe_Iio 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Iio PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	Set.preimage_comp WithBot.preimage_coe_Iio WithTop.preimage_coe_Iio
preimage_coe_Iio_top 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Iio PartialOrder.toPreorder instPartialOrderEReal Top.top instTop Set.univ	—	Set.preimage_comp WithBot.preimage_coe_Iio WithTop.preimage_coe_Iio_top
preimage_coe_Ioc 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioc PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	preimage_coe_Ioi preimage_coe_Iic
preimage_coe_Ioc_bot 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioc PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Set.Iic Real.instPreorder	—	Set.Ioi_inter_Iic preimage_coe_Ioi_bot preimage_coe_Iic Set.univ_inter
preimage_coe_Ioi 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioi PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	Set.preimage_comp WithBot.preimage_coe_Ioi WithTop.preimage_coe_Ioi
preimage_coe_Ioi_bot 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioi PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Set.univ	—	Set.preimage_comp WithBot.preimage_coe_Ioi_bot
preimage_coe_Ioo 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Real.instPreorder	—	preimage_coe_Ioi preimage_coe_Iio
preimage_coe_Ioo_bot 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Set.Iio Real.instPreorder	—	Set.Ioi_inter_Iio preimage_coe_Ioi_bot preimage_coe_Iio Set.univ_inter
preimage_coe_Ioo_bot_top 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Top.top instTop Set.univ	—	Set.Ioi_inter_Iio preimage_coe_Ioi_bot preimage_coe_Iio_top Set.inter_self
preimage_coe_Ioo_top 📖	mathematical	—	Set.preimage Real EReal Real.toEReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Top.top instTop Set.Ioi Real.instPreorder	—	Set.Ioi_inter_Iio preimage_coe_Ioi preimage_coe_Iio_top Set.inter_univ
range_coe 📖	mathematical	—	Set.range EReal Real Real.toEReal Compl.compl Set Set.instCompl Set.instInsert Bot.bot instBotEReal Set.instSingletonSet Top.top instTop	—	Set.ext
range_coe_ennreal 📖	mathematical	—	Set.range EReal ENNReal ENNReal.toEReal Set.Ici PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	—	Set.Subset.antisymm Set.range_subset_iff coe_ennreal_nonneg LT.lt.not_ge bot_lt_zero coe_nonneg
range_coe_eq_Ioo 📖	mathematical	—	Set.range EReal Real Real.toEReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal Top.top instTop	—	Set.ext
real_coe_toENNReal 📖	mathematical	—	toENNReal Real.toEReal ENNReal.ofReal	—	—
toENNReal_bot 📖	mathematical	—	toENNReal Bot.bot EReal instBotEReal ENNReal instZeroENNReal	—	toENNReal_of_nonpos bot_le
toENNReal_coe 📖	mathematical	—	toENNReal ENNReal.toEReal	—	coe_ennreal_top toENNReal_top toENNReal.eq_1 toReal_coe_ennreal ENNReal.ofReal_toReal_eq_iff
toENNReal_eq_toENNReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	toENNReal	—	toENNReal_of_ne_top
toENNReal_eq_top_iff 📖	mathematical	—	toENNReal Top.top ENNReal instTopENNReal EReal instTop	—	—
toENNReal_eq_zero_iff 📖	mathematical	—	toENNReal ENNReal instZeroENNReal EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	—	ENNReal.ofReal_zero
toENNReal_le_toENNReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal	ENNReal ENNReal.instPartialOrder toENNReal	—	toENNReal_of_ne_top ENNReal.ofReal_zero ENNReal.instCanonicallyOrderedAdd ENNReal.ofReal_le_ofReal toReal_le_toReal coe_ne_bot
toENNReal_lt_toENNReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal Preorder.toLT	ENNReal ENNReal.instPartialOrder toENNReal	—	lt_of_le_of_ne toENNReal_le_toENNReal LT.lt.le LT.lt.ne toENNReal_eq_toENNReal LE.le.trans_lt
toENNReal_ne_top_iff 📖	—	—	—	—	Iff.not toENNReal_eq_top_iff
toENNReal_ne_zero_iff 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	—	Iff.not toENNReal_eq_zero_iff
toENNReal_of_ne_top 📖	mathematical	—	toENNReal ENNReal.ofReal toReal	—	—
toENNReal_of_nonpos 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	toENNReal ENNReal instZeroENNReal	—	toENNReal.eq_1 zero_ne_top top_le_iff ENNReal.ofReal_of_nonpos toReal_nonpos
toENNReal_pos_iff 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal toENNReal EReal instPartialOrderEReal instZeroEReal	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd toENNReal_ne_zero_iff
toENNReal_top 📖	mathematical	—	toENNReal Top.top EReal instTop ENNReal instTopENNReal	—	—
toENNReal_zero 📖	mathematical	—	toENNReal EReal instZeroEReal ENNReal instZeroENNReal	—	toENNReal_of_nonpos le_rfl
toReal_bot 📖	mathematical	—	toReal Bot.bot EReal instBotEReal Real Real.instZero	—	—
toReal_coe 📖	mathematical	—	toReal Real.toEReal	—	—
toReal_coe_ennreal 📖	mathematical	—	toReal ENNReal.toEReal ENNReal.toReal	—	—
toReal_eq_toReal 📖	mathematical	—	toReal	—	CanLift.prf canLift
toReal_eq_zero_iff 📖	mathematical	—	toReal Real Real.instZero EReal instZeroEReal Top.top instTop Bot.bot instBotEReal	—	—
toReal_image_Ioo_bot_zero 📖	mathematical	—	Set.image EReal Real toReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal Bot.bot instBotEReal instZeroEReal Set.Iio Real.instPreorder Real.instZero	—	Set.ext CanLift.prf canLift
toReal_image_Ioo_zero_top 📖	mathematical	—	Set.image EReal Real toReal Set.Ioo PartialOrder.toPreorder instPartialOrderEReal instZeroEReal Top.top instTop Set.Ioi Real.instPreorder Real.instZero	—	Set.ext CanLift.prf canLift
toReal_le_toReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal	Real Real.instLE toReal	—	CanLift.prf canLift ne_top_of_le_ne_top ne_bot_of_le_ne_bot
toReal_ne_zero_iff 📖	—	—	—	—	—
toReal_neg 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	Real Real.instLT toReal Real.instZero	—	CanLift.prf canLift
toReal_nonneg 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	Real Real.instLE Real.instZero toReal	—	coe_nonneg toReal_coe
toReal_nonpos 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	Real Real.instLE toReal Real.instZero	—	coe_nonpos toReal_coe
toReal_one 📖	mathematical	—	toReal EReal instOneEReal Real Real.instOne	—	—
toReal_pos 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	Real Real.instLT Real.instZero toReal	—	CanLift.prf canLift
toReal_toENNReal 📖	mathematical	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal	ENNReal.toReal toENNReal toReal	—	toENNReal_of_ne_top ENNReal.toReal_ofReal toReal_nonneg
toReal_top 📖	mathematical	—	toReal Top.top EReal instTop Real Real.instZero	—	—
toReal_zero 📖	mathematical	—	toReal EReal instZeroEReal Real Real.instZero	—	—
top_ne_coe 📖	—	—	—	—	LT.lt.ne' coe_lt_top
top_ne_zero 📖	—	—	—	—	coe_ne_top
zero_lt_top 📖	mathematical	—	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal instZeroEReal Top.top instTop	—	coe_lt_top
zero_mul 📖	mathematical	—	EReal instMul instZeroEReal	—	lt_irrefl MulZeroClass.zero_mul
zero_ne_bot 📖	—	—	—	—	coe_ne_bot
zero_ne_top 📖	—	—	—	—	coe_ne_top

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalENNRealToEReal 📖	CompOp	—
evalERealToENNReal 📖	CompOp	—
evalERealToReal 📖	CompOp	—
evalRealToEReal 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
toEReal 📖	CompOp	152 math math: EReal.nhds_top_basis, EReal.continuousAt_add_coe_bot, EReal.real_coe_toENNReal, Complex.isOpen_re_lt_EReal, EReal.coe_le_coe_iff, EReal.continuousAt_add_coe_top, EReal.image_coe_Icc, EReal.bot_mul_coe_of_neg, ENNReal.log_pos_real', EReal.bot_mul_coe_of_pos, EReal.image_coe_Ioc, EReal.continuousAt_add_coe_coe, EReal.coe_coe_eq_natCast, EReal.forall, EReal.addLECancellable_coe, EReal.image_coe_Ico, LSeriesSummable.abscissaOfAbsConv_le, EReal.nhds_coe, EReal.preimage_coe_Ioi, EReal.image_coe_Iio, EReal.le_coe_toReal, EReal.coe_nonpos, EReal.isOpenEmbedding_coe, EReal.top_mul_coe_of_pos, EReal.add_lt_add_left_coe, EReal.preimage_coe_Ioo, EReal.tendsto_coe_atTop, EReal.coe_neg, EReal.nhds_bot_basis, LSeries_deriv_eqOn, EReal.sub_add_cancel_left, LSeries_analyticOnNhd, EReal.nhds_top', EReal.canLift, EReal.bot_lt_coe, EReal.preimage_coe_Ioo_top, EReal.coe_natCast, EReal.mem_nhds_bot_iff, EReal.range_coe_eq_Ioo, EReal.image_coe_Iic, EReal.coe_sub, EReal.coe_zsmul, ENNReal.log_of_nnreal, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, EReal.preimage_coe_Icc, EReal.sub_add_cancel, ENNReal.log_pos_real, EReal.sign_coe, EReal.coe_le_coe, EReal.abs_coe_lt_top, EReal.add_sub_cancel_left, EReal.coe_zero, EReal.ge_of_forall_gt_iff_ge, EReal.top_sub_coe, EReal.eq_bot_iff_forall_lt, EReal.exp_coe, EReal.range_coe, EReal.continuousAt_add_bot_coe, EReal.preimage_coe_Ici, EReal.image_coe_Ioo, EReal.ENNReal.rpow_eq_exp_mul_log, EReal.coe_coe_sign, EReal.preimage_coe_Ioi_bot, EReal.preimage_coe_Ioc, continuous_coe_real_ereal, EReal.image_coe_Ici, EReal.coe_neg', EReal.coe_toReal, EReal.coe_mul_top_of_pos, EReal.coe_eq_coe_iff, EReal.top_add_coe, EReal.add_sub_cancel_right, EReal.tendsto_coe, EReal.coe_nonneg, EReal.preimage_coe_Ioo_bot, EReal.coe_injective, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, EReal.coe_strictMono, EReal.coe_add_top, EReal.preimage_coe_Ico_top, LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow, EReal.tendsto_coe_nhds_bot_iff, EReal.tendsto_coe_atBot, Complex.isOpen_im_gt_EReal, EReal.exists, LSeries_differentiableOn, EReal.continuousAt_add_top_coe, EReal.toReal_coe, EReal.preimage_coe_Iio, ENNReal.log_rpow, EReal.coe_ennreal_toReal, EReal.continuous_coe_iff, EReal.preimage_coe_Ioo_bot_top, EReal.tendsto_coe_nhds_top_iff, EReal.coe_pos, EReal.le_of_forall_lt_iff_le, measurable_coe_real_ereal, EReal.preimage_coe_Iio_top, EReal.coe_eq_zero, EReal.nhds_bot', Complex.isOpen_im_lt_EReal, EReal.exp_mul, EReal.tendsto_nhds_top_iff_real, EReal.coe_nsmul, LSeries_analyticOn, EReal.coe_mul, EReal.abs_def, EReal.coe_nnreal_eq_coe_real, EReal.preimage_coe_Iic, EReal.sub_add_cancel_right, EReal.coe_mul_bot_of_neg, EReal.coe_lt_coe, EReal.coe_add, EReal.coe_pow, EReal.coe_one, EReal.lt_iff_exists_rat_btwn, EReal.preimage_coe_Ioc_bot, EReal.coe_inv, EReal.coe_eq_one, EReal.preimage_coe_Ico, EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal, EReal.coe_sub_bot, EReal.coe_div, EReal.coe_abs, EReal.measurableEmbedding_coe, EReal.isEmbedding_coe, EReal.add_lt_add_right_coe, EReal.coe_mul_bot_of_pos, EReal.denseRange_ratCast, Measurable.coe_real_ereal, EReal.nhds_coe_coe, ENNReal.log_ofReal_of_pos, EReal.exists_between_coe_real, EReal.coe_ennreal_ofReal, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, EReal.nhdsWithin_top, EReal.image_coe_Ioi, EReal.exists_rat_btwn_of_lt, EReal.eq_top_iff_forall_lt, EReal.nhdsWithin_bot, Complex.isOpen_re_gt_EReal, EReal.coe_mul_top_of_neg, EReal.coe_toReal_le, AEMeasurable.coe_real_ereal, EReal.coe_lt_coe_iff, EReal.mem_nhds_top_iff, EReal.coe_lt_top, LSeries.abscissaOfAbsConv_le_of_isBigO_rpow, EReal.tendsto_nhds_bot_iff_real, EReal.lt_iff_exists_real_btwn, ENNReal.log_ofReal, EReal.top_mul_coe_of_neg

(root)

Definitions

Name	Category	Theorems
EReal 📖	CompOp	558 math math: EReal.nhds_top_basis, LinearGrowth.linearGrowthSup_zero, LinearGrowth.linearGrowthSup_top, EReal.continuousAt_add_coe_bot, Dynamics.netEntropyEntourage_monotone, Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage, EReal.exp_bot, Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage, EReal.one_lt_exp_iff, EReal.inv_strictAntiOn, Complex.isOpen_re_lt_EReal, EReal.coe_le_coe_iff, LSeries.abscissaOfAbsConv_one, Dynamics.coverEntropyInfEntourage_antitone, EReal.continuousAt_add_coe_top, EReal.image_coe_Icc, EReal.bot_mul_coe_of_neg, ENNReal.log_lt_log_iff, EReal.natCast_mul, EReal.div_eq_inv_mul, EReal.coe_ennreal_add, Monotone.expGrowthSup_nonneg, EReal.coe_ennreal_le_coe_ennreal_iff, EReal.sub_nonneg, EReal.neg_nonneg, EReal.abs_neg, EReal.instMeasurableMul₂, LinearGrowth.linearGrowthInf_add_le', ENNReal.log_eq_bot_iff, LinearGrowth.le_linearGrowthSup_add, EReal.mul_nonpos_iff, EReal.sub_top, EReal.bot_mul_coe_of_pos, EReal.toENNReal_eq_zero_iff, ENNReal.log_le_log_iff, EReal.toENNReal_top, LinearGrowth.linearGrowthSup_add_le, EReal.image_coe_Ioc, measurable_ereal_toENNReal, EReal.exp_strictMono, ExpGrowth.expGrowthInf_of_eventually_ge, EReal.continuousAt_add_coe_coe, ENNReal.log_lt_zero_iff, EReal.coe_ennreal_pow, LSeries_injOn, EReal.coe_coe_eq_natCast, EReal.measurable_exp, LSeries_eventually_eq_zero_iff', EReal.forall, ExpGrowth.expGrowthInf_exp, Monotone.expGrowthInf_comp_mul, EReal.div_mul_div_comm, EReal.neg_strictAnti, Dynamics.coverEntropy_iUnion_le, EReal.addLECancellable_coe, ExpGrowth.expGrowthInf_le_iff, EReal.image_coe_Ico, LSeriesSummable.abscissaOfAbsConv_le, EReal.instT2Space, EReal.neg_lt_comm, EReal.toENNReal_pos_iff, measurable_ereal_toReal, EReal.top_sub, EReal.nhds_coe, EReal.sign_eq_and_abs_eq_iff_eq, LinearGrowth.le_linearGrowthSup_add', Dynamics.netEntropyInfEntourage_univ, ExpGrowth.expGrowthSup_add, Dynamics.coverEntropyInfEntourage_univ, EReal.preimage_coe_Ioi, EReal.neg_eq_top_iff, LinearGrowth.linearGrowthInf_bot, Dynamics.netEntropyEntourage_le_coverEntropyEntourage, EReal.continuousAt_add_bot_bot, EReal.abs_eq_zero_iff, EReal.instPosMulMono, EReal.expOrderIso_symm, Dynamics.coverEntropyEntourage_univ, EReal.image_coe_Iio, ArithmeticFunction.abscissaOfAbsConv_zeta, EReal.coe_ennreal_mul_top, EReal.le_coe_toReal, ExpGrowth.expGrowthInf_eventually_monotone, EReal.iSup_add_le_add_iSup, EReal.sub_self, EReal.coe_nonpos, LinearGrowth.linearGrowthSup_bot, EReal.isOpenEmbedding_coe, EReal.top_mul_coe_of_pos, EReal.add_lt_top, ENNReal.continuous_log, ExpGrowth.expGrowthSup_sum, LinearGrowth.linearGrowthInf_biInf, EReal.tendsto_exp_nhds_zero_nhds_one, EReal.neg_le_neg_iff, EReal.top_mul_coe_ennreal, EReal.preimage_coe_Ioo, Dynamics.coverEntropy_monotone, ExpGrowth.expGrowthSup_def, EReal.tendsto_coe_atTop, EReal.isClosedEmbedding_coe_ennreal, EReal.coe_neg, ENNReal.log_top, EReal.bot_add, ExpGrowth.expGrowthSup_biSup, ENNReal.log_strictMono, ExpGrowth.expGrowthInf_mul_le, EReal.nhds_bot_basis, LSeries_deriv_eqOn, EReal.sub_add_cancel_left, LSeries.abscissaOfAbsConv_le_of_le_const, EReal.one_le_exp_iff, LSeries_analyticOnNhd, Dynamics.netEntropyEntourage_antitone, EReal.exists_nat_ge_mul, EReal.neg_sub, EReal.nhds_top', EReal.canLift, EReal.bot_lt_coe, EReal.abs_mul_sign, Dynamics.coverEntropyEntourage_union, LinearGrowth.linearGrowthInf_top, Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage, EReal.instMeasurableAdd₂, EReal.inv_inv, ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, EReal.preimage_coe_Ioo_top, EReal.toReal_zero, EReal.limsup_neg, EReal.mul_div_mul_cancel, EReal.bot_lt_add_iff, EReal.instMulPosMono, EReal.coe_natCast, EReal.tendsto_toReal_atTop, EReal.top_add_of_ne_bot, EReal.instT5Space, EReal.tendsto_toReal_atBot, LinearGrowth.linearGrowthInf_const_mul_self, Dynamics.coverEntropyEntourage_le_netEntropyEntourage, EReal.one_mul, ExpGrowth.expGrowthInf_comp_nonneg, EReal.mem_nhds_bot_iff, EReal.add_bot, EReal.range_coe_ennreal, EReal.top_sub_bot, Dynamics.netEntropyEntourage_empty, ExpGrowth.expGrowthInf_inv, ExpGrowth.expGrowthSup_inv, Dynamics.coverEntropy_union, EReal.range_coe_eq_Ioo, LinearGrowth.linearGrowthInf_zero, EReal.neg_eq_zero_iff, ExpGrowth.expGrowthInf_le_expGrowthSup_of_frequently_le, EReal.image_coe_Iic, Dynamics.coverEntropyInfEntourage_le_coverEntropyInf, Dynamics.netEntropyInfEntourage_nonneg, EReal.instCanLiftENNRealToERealLeOfNat, EReal.measurable_of_measurable_real, EReal.abs_top, Measurable.coe_ereal_ennreal, EReal.coe_sub, EReal.coe_ennreal_zero, ENNReal.log_le_log, Dynamics.netEntropyInfEntourage_le_netEntropyEntourage, EReal.toENNReal_eq_top_iff, LSeries.abscissaOfAbsConv_le_one_of_isBigO_one, Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage, EReal.coe_zsmul, ExpGrowth.expGrowthInf_monotone, Dynamics.coverEntropyEntourage_image_le, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, EReal.tendsto_coe_ennreal, EReal.expHomeomorph_symm, EReal.preimage_coe_Icc, EReal.sign_mul, ENNReal.zero_lt_log_iff, Dynamics.coverEntropyInf_image_le_of_uniformContinuous, EReal.bot_sub, EReal.sub_add_cancel, EReal.bot_mul_bot, EReal.min_neg_neg, ENNReal.log_eq_one_iff, LinearGrowth.linearGrowthSup_biSup, EReal.exp_lt_exp_iff, EReal.sign_coe, EReal.le_liminf_add, EReal.inv_neg, EReal.neg_add, ExpGrowth.expGrowthSup_const, ENNReal.logOrderIso_symm, EReal.exp_monotone, LinearGrowth.linearGrowthSup_inv, EReal.coe_le_coe, LinearGrowth.linearGrowthInf_const, EReal.mul_div, EReal.mul_ne_top, ENNReal.log_monotone, EReal.liminf_add_le, EReal.nsmul_eq_mul, EReal.add_sub_cancel_left, LinearGrowth.linearGrowthSup_le_iff, ExpGrowth.le_expGrowthInf_comp, EReal.coe_zero, EReal.ge_of_forall_gt_iff_ge, Dynamics.coverEntropy_biUnion_finset, LinearGrowth.linearGrowthSup_const_mul_self, EReal.instSecondCountableTopology, EReal.top_sub_coe, Dynamics.le_coverEntropyEntourage_image, EReal.eq_bot_iff_forall_lt, EReal.tendsto_const_div_atTop_nhds_zero_nat, Dynamics.coverEntropyEntourage_monotone, EReal.range_coe, EReal.mul_ne_bot, EReal.mul_nonneg_iff, EReal.continuousAt_add_bot_coe, EReal.top_add_iff_ne_bot, EReal.abs_mul, Dynamics.coverEntropy_antitone, EReal.sub_lt_iff, ExpGrowth.expGrowthInf_le_of_eventually_le, Measurable.ennreal_log, EReal.preimage_coe_Ici, EReal.image_coe_Ioo, EReal.natCast_lt_iff, Dynamics.coverEntropyInf_monotone, ENNReal.log_surjective, EReal.continuousOn_toReal, EReal.exp_eq_top_iff, ExpGrowth.expGrowthSup_zero, LinearGrowth.linearGrowthSup_sup, continuous_coe_ennreal_ereal, EReal.toReal_neg_eq, Dynamics.coverEntropy_iUnion_of_finite, EReal.ENNReal.rpow_eq_exp_mul_log, EReal.mul_neg_iff, ExpGrowth.expGrowthSup_exp, EReal.tendsto_exp_nhds_top_nhds_top, ExpGrowth.expGrowthSup_of_eventually_ge, LinearGrowth.linearGrowthInf_inf, EReal.coe_coe_sign, EReal.preimage_coe_Ioi_bot, EReal.neg_lt_zero, EReal.coe_toENNReal_eq_max, EReal.bot_lt_zero, EReal.div_zero, EReal.preimage_coe_Ioc, Dynamics.netEntropyInfEntourage_monotone, continuous_coe_real_ereal, EReal.image_coe_Ici, EReal.toReal_top, EReal.coe_neg', Dynamics.coverEntropyInf_nonneg, Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div, Dynamics.coverEntropyEntourage_finite_of_isCompact_invariant, LinearGrowth.linearGrowthSup_const, EReal.coe_ennreal_eq_zero, LSeries.abscissaOfAbsConv_binop_le, EReal.sign_bot, EReal.bot_lt_inv, LSeries.abscissaOfAbsConv_add_le, EReal.add_top_of_ne_bot, ExpGrowth.expGrowthSup_mul_le, ENNReal.log_bijective, LinearGrowth.linearGrowthInf_natCast_nonneg, ExpGrowth.expGrowthInf_inf, Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariant, measurable_coe_ennreal_ereal, EReal.coe_mul_top_of_pos, EReal.top_add_coe, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable', EReal.exp_le_one_iff, EReal.sub_nonpos, EReal.natCast_eq_iff, EReal.le_neg, EReal.bot_lt_coe_ennreal, EReal.toReal_add, ENNReal.log_pow, Dynamics.coverEntropyInf_antitone, EReal.add_sub_cancel_right, Dynamics.coverEntropyEntourage_le_log_coverMincard_div, EReal.add_iInf_le_iInf_add, EReal.tendsto_coe, EReal.neg_le_zero, EReal.coe_nonneg, ExpGrowth.le_expGrowthInf_add, EReal.toReal_image_Ioo_bot_zero, EReal.neg_eq_bot_iff, LSeries.abscissaOfAbsConv_convolution_le, Dynamics.coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, EReal.zero_lt_exp_iff, EReal.tendsto_exp_nhds_bot_nhds_zero, EReal.preimage_coe_Ioo_bot, ENNReal.log_lt_top_iff, DirichletCharacter.absicssaOfAbsConv_eq_one, ExpGrowth.le_expGrowthInf_iff, ExpGrowth.expGrowthSup_comp_le, EReal.abs_zero, EReal.coe_injective, EReal.div_self, EReal.bot_mul_top, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, EReal.sub_self_le_zero, EReal.coe_ennreal_eq_one, EReal.coe_strictMono, EReal.coe_ennreal_lt_coe_ennreal_iff, Dynamics.coverEntropy_image_le_of_uniformContinuous, ExpGrowth.expGrowthSup_comp_nonneg, EReal.coe_add_top, ENNReal.log_le_zero_iff, EReal.liminf_neg, EReal.preimage_coe_Ico_top, LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow, ENNReal.continuous_exp, EReal.tendsto_coe_nhds_bot_iff, EReal.sub_neg, EReal.tendsto_coe_atBot, Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage, ExpGrowth.expGrowthInf_iInf, Complex.isOpen_im_gt_EReal, ExpGrowth.expGrowthSup_eventually_monotone, EReal.max_neg_neg, instPolishSpaceEReal, EReal.exists, EReal.toReal_bot, LSeries_differentiableOn, EReal.inv_top, EReal.top_mul_bot, Monotone.expGrowthInf_comp_le, EReal.sub_bot, Dynamics.coverEntropy_nonneg, EReal.instNoZeroDivisors, EReal.continuousAt_add_top_coe, EReal.borelSpace, Dynamics.coverEntropyEntourage_antitone, EReal.sign_top, LinearGrowth.linearGrowthInf_iInf, EReal.toENNReal_zero, EReal.preimage_coe_Iio, ENNReal.log_rpow, EReal.continuous_coe_iff, EReal.continuous_toENNReal, EReal.mul_comm, ENNReal.log_eq_top_iff, EReal.preimage_coe_Ioo_bot_top, ENNReal.measurable_log, EReal.toENNReal_bot, EReal.lt_sub_iff_add_lt, Monotone.expGrowthInf_nonneg, EReal.exp_zero, EReal.tendsto_coe_nhds_top_iff, ExpGrowth.expGrowthInf_biInf, LinearGrowth.linearGrowthSup_iSup, Dynamics.coverEntropy_eq_iSup_basis, ENNReal.zero_le_log_iff, EReal.instMulPosReflectLT, EReal.div_top, EReal.neg_pos, EReal.coe_pos, EReal.mul_div_cancel, EReal.le_iff_sign, Dynamics.coverEntropy_eq_iSup_basis_netEntropyEntourage, EReal.mul_eq_bot, EReal.toReal_mul, EReal.isEmbedding_coe_ennreal, EReal.le_of_forall_lt_iff_le, ENNReal.toEReal_sub, measurable_coe_real_ereal, EReal.preimage_coe_Iio_top, Dynamics.coverEntropy_biUnion_le, ENNReal.log_one, AEMeasurable.coe_ereal_ennreal, EReal.coe_eq_zero, EReal.nhds_bot', EReal.inv_bot, EReal.toReal_one, ENNReal.log_zero, Complex.isOpen_im_lt_EReal, Dynamics.coverEntropyEntourage_nonneg, EReal.exp_mul, ENNReal.logHomeomorph_symm, Dynamics.netEntropyInfEntourage_le_coverEntropyInf, LinearGrowth.le_linearGrowthInf_iff, EReal.tendsto_nhds_top_iff_real, EReal.nhds_bot, EReal.coe_nsmul, ExpGrowth.le_expGrowthSup_mul', Dynamics.coverEntropyInfEntourage_image_le, Dynamics.coverEntropy_eq_iSup_netEntropyEntourage, LSeries_analyticOn, EReal.lt_neg_comm, EReal.exp_lt_one_iff, EReal.lowerSemicontinuous_add, EReal.toReal_image_Ioo_zero_top, EReal.coe_mul, EReal.inv_lt_top, ExpGrowth.expGrowthInf_def, Dynamics.coverEntropyInfEntourage_closure, ExpGrowth.expGrowthInf_mul_le', EReal.coe_ennreal_injective, LinearGrowth.linearGrowthInf_le_iff, EReal.le_limsup_add, Dynamics.coverEntropyEntourage_closure, EReal.top_mul_top, Dynamics.netEntropyInfEntourage_empty, EReal.mul_div_left_comm, Dynamics.coverEntropyInf_iUnion_le, EReal.preimage_coe_Iic, ENNReal.log_injective, EReal.exp_nmul, ExpGrowth.expGrowthSup_top, EReal.continuousAt_add, EReal.toENNReal_ne_zero_iff, ExpGrowth.expGrowthInf_const, Dynamics.coverEntropyInf_empty, LSeries.abscissaOfAbsConv_sub_le, EReal.sub_add_cancel_right, EReal.coe_mul_bot_of_neg, EReal.coe_lt_coe, EReal.tendsto_toReal, EReal.exp_lt_top_iff, EReal.coe_add, EReal.zero_div, EReal.expOrderIso_apply, ENNReal.bot_lt_log_iff, EReal.coe_pow, EReal.coe_one, EReal.continuousAt_add_top_top, EReal.toReal_eq_zero_iff, EReal.exp_add, EReal.sign_mul_inv_abs, Dynamics.netEntropyEntourage_nonneg, EReal.coe_ennreal_strictMono, EReal.lt_iff_exists_rat_btwn, EReal.preimage_coe_Ioc_bot, LinearGrowth.linearGrowthInf_add_le, EReal.coe_inv, EReal.coe_eq_one, ENNReal.logHomeomorph_apply, Dynamics.coverEntropyInf_biUnion_le, EReal.div_mul_cancel, ExpGrowth.expGrowthSup_le_iff, EReal.sign_mul_abs, EReal.sub_pos, ExpGrowth.expGrowthInf_top, Dynamics.coverEntropyEntourage_le_coverEntropy, EReal.coe_ennreal_one, EReal.sub_le_iff_le_add, EReal.natCast_div_le, EReal.preimage_coe_Ico, EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal, EReal.nhds_top, instIsOrderedAddMonoidEReal, EReal.coe_sub_bot, EReal.mul_div_right, Dynamics.netEntropyEntourage_le_coverEntropy, EReal.coe_div, EReal.tendsto_mul, EReal.measurableEmbedding_coe, Dynamics.coverEntropyInf_image_le_of_uniformContinuousOn_invariant, EReal.top_add_top, EReal.mul_pos_iff, EReal.isEmbedding_coe, EReal.coe_mul_bot_of_pos, EReal.denseRange_ratCast, EReal.toReal_sub, EReal.exp_eq_zero_iff, EReal.sign_neg, EReal.mul_inv, Dynamics.le_coverEntropyInfEntourage_image, EReal.continuous_coe_ennreal_iff, EReal.div_eq_iff, EReal.abs_bot, ExpGrowth.expGrowthSup_sup, EReal.zero_lt_top, ENNReal.log_mul_add, Measurable.coe_real_ereal, EReal.add_top_iff_ne_bot, ExpGrowth.expGrowthSup_le_of_eventually_le, Dynamics.netEntropyInfEntourage_antitone, ExpGrowth.expGrowthInf_zero, EReal.neg_le, EReal.nhds_coe_coe, EReal.zero_mul, EReal.coe_ennreal_nsmul, ENNReal.log_lt_log, EReal.coe_ennreal_nonneg, EReal.coe_nnreal_lt_top, ENNReal.log_inv, EReal.neg_mul, Monotone.expGrowthSup_comp_mul, EReal.coe_ennreal_pos_iff_ne_zero, EReal.coe_ennreal_mul, instZeroLEOneClassEReal, EReal.continuousAt_mul, Dynamics.coverEntropyInfEntourage_nonneg, Dynamics.coverEntropyEntourage_empty, ExpGrowth.le_expGrowthSup_mul, Dynamics.coverEntropy_empty, Dynamics.coverEntropyInfEntourage_empty, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, EReal.instContinuousNeg, EReal.nhdsWithin_top, ExpGrowth.expGrowthSup_iSup, EReal.image_coe_Ioi, EReal.le_sub_iff_add_le, EReal.add_eq_bot_iff, instDenselyOrderedEReal, EReal.expHomeomorph_apply, instCharZeroEReal, EReal.mul_eq_top, ExpGrowth.le_expGrowthInf_mul, LinearGrowth.le_linearGrowthSup_iff, ExpGrowth.le_expGrowthSup_iff, ExpGrowth.expGrowthInf_le_expGrowthSup, EReal.exp_le_exp_iff, EReal.natCast_le_iff, LSeries_eq_zero_iff, Dynamics.coverEntropyInf_eq_iSup_basis, EReal.eq_top_iff_forall_lt, EReal.neg_top, EReal.nhdsWithin_bot, Complex.isOpen_re_gt_EReal, EReal.sign_mul_inv_abs', ENNReal.logOrderIso_apply, ExpGrowth.expGrowthSup_monotone, EReal.div_div, Dynamics.coverEntropyInfEntourage_monotone, EReal.coe_ennreal_eq_top_iff, EReal.coe_mul_top_of_neg, EReal.toENNReal_add_le, EReal.div_bot, EReal.coe_ennreal_top, LinearGrowth.le_linearGrowthInf_add, EReal.inv_zero, EReal.neg_bot, EReal.exp_neg, EReal.coe_toReal_le, EReal.exp_top, AEMeasurable.coe_real_ereal, EReal.coe_lt_coe_iff, EReal.mem_nhds_top_iff, Dynamics.coverEntropyInf_le_coverEntropy, EReal.limsup_add_le, EReal.coe_lt_top, Dynamics.netEntropyEntourage_univ, EReal.instOrderTopology, EReal.neg_lt_neg_iff, EReal.coe_ennreal_pos, LSeries.abscissaOfAbsConv_le_of_isBigO_rpow, EReal.tendsto_nhds_bot_iff_real, EReal.instPosMulReflectLT, EReal.lt_iff_exists_real_btwn, ArithmeticFunction.abscissaOfAbsConv_moebius, ENNReal.log_ofReal, EReal.top_mul_coe_of_neg, LinearGrowth.linearGrowthInf_neg, Monotone.le_expGrowthSup_comp
instAddCommMonoidEReal 📖	CompOp	81 math math: EReal.continuousAt_add_coe_bot, EReal.continuousAt_add_coe_top, EReal.coe_ennreal_add, LinearGrowth.linearGrowthInf_add_le', EReal.liminf_add_top_of_ne_bot, LinearGrowth.le_linearGrowthSup_add, LinearGrowth.linearGrowthSup_add_le, EReal.continuousAt_add_coe_coe, EReal.left_distrib_of_nonneg, EReal.addLECancellable_coe, EReal.add_lt_add_of_lt_of_le', LinearGrowth.le_linearGrowthSup_add', EReal.continuousAt_add_bot_bot, EReal.add_pos_of_pos_of_nonneg, EReal.iSup_add_le_add_iSup, EReal.add_lt_add_left_coe, EReal.add_lt_top, EReal.bot_add, ExpGrowth.expGrowthInf_mul_le, EReal.sub_add_cancel_left, EReal.neg_sub, EReal.instMeasurableAdd₂, EReal.bot_lt_add_iff, EReal.top_add_of_ne_bot, EReal.add_bot, EReal.right_distrib_of_nonneg_of_ne_top, EReal.sub_add_cancel, EReal.le_liminf_add, EReal.neg_add, EReal.add_le_of_le_sub, EReal.liminf_add_le, EReal.add_sub_cancel_left, EReal.continuousAt_add_bot_coe, EReal.top_add_iff_ne_bot, EReal.sub_lt_iff, EReal.add_pos, EReal.add_top_of_ne_bot, ExpGrowth.expGrowthSup_mul_le, EReal.top_add_coe, EReal.toReal_add, EReal.add_sub_cancel_right, EReal.add_iInf_le_iInf_add, EReal.add_lt_add_of_lt_of_le, EReal.coe_add_top, LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow, EReal.continuousAt_add_top_coe, EReal.lt_sub_iff_add_lt, ExpGrowth.le_expGrowthSup_mul', EReal.lowerSemicontinuous_add, ExpGrowth.expGrowthInf_mul_le', EReal.add_div_of_nonneg_right, EReal.le_limsup_add, EReal.left_distrib_of_nonneg_of_ne_top, EReal.continuousAt_add, EReal.sub_add_cancel_right, EReal.toENNReal_add, EReal.coe_add, EReal.continuousAt_add_top_top, EReal.exp_add, LinearGrowth.linearGrowthInf_add_le, EReal.sub_le_iff_le_add, instIsOrderedAddMonoidEReal, EReal.add_lt_add, EReal.top_add_top, EReal.add_lt_add_right_coe, EReal.right_distrib_of_nonneg, EReal.div_right_distrib_of_nonneg, ENNReal.log_mul_add, EReal.liminf_add_gt_of_gt, EReal.add_top_iff_ne_bot, EReal.limsup_add_bot_of_ne_top, EReal.add_lt_of_lt_sub, ExpGrowth.le_expGrowthSup_mul, EReal.le_sub_iff_add_le, EReal.add_eq_bot_iff, ExpGrowth.le_expGrowthInf_mul, EReal.limsup_add_le_of_le, EReal.toENNReal_add_le, LinearGrowth.le_linearGrowthInf_add, EReal.limsup_add_le, LSeries.abscissaOfAbsConv_le_of_isBigO_rpow
instAddCommMonoidWithOneEReal 📖	CompOp	80 math math: LinearGrowth.linearGrowthSup_zero, LinearGrowth.linearGrowthSup_top, EReal.natCast_mul, ExpGrowth.eventually_le_exp, LinearGrowth.linearGrowthInf_add_le', LinearGrowth.le_linearGrowthSup_add, LinearGrowth.linearGrowthSup_add_le, EReal.coe_coe_eq_natCast, ExpGrowth.expGrowthInf_exp, Monotone.expGrowthInf_comp_mul, ExpGrowth.expGrowthInf_le_iff, LinearGrowth.le_linearGrowthSup_add', LinearGrowth.linearGrowthInf_bot, LinearGrowth.linearGrowthSup_bot, LinearGrowth.linearGrowthInf_biInf, ExpGrowth.expGrowthSup_def, EReal.exists_nat_ge_mul, LinearGrowth.linearGrowthInf_top, EReal.coe_natCast, LinearGrowth.linearGrowthInf_const_mul_self, LinearGrowth.linearGrowthInf_zero, LinearGrowth.linearGrowthSup_le_of_eventually_le, LinearGrowth.linearGrowthSup_biSup, LinearGrowth.linearGrowthSup_inv, LinearGrowth.linearGrowthInf_const, EReal.nsmul_eq_mul, LinearGrowth.linearGrowthSup_le_iff, ExpGrowth.le_expGrowthInf_comp, LinearGrowth.linearGrowthSup_const_mul_self, EReal.tendsto_const_div_atTop_nhds_zero_nat, EReal.natCast_lt_iff, LinearGrowth.linearGrowthSup_sup, ExpGrowth.expGrowthSup_exp, LinearGrowth.linearGrowthInf_inf, Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div, LinearGrowth.linearGrowthSup_eventually_monotone, LinearGrowth.linearGrowthSup_const, LinearGrowth.linearGrowthInf_natCast_nonneg, LinearGrowth.linearGrowthSup_comp_nonneg, EReal.natCast_eq_iff, ENNReal.log_pow, Dynamics.coverEntropyEntourage_le_log_coverMincard_div, Monotone.linearGrowthInf_nonneg, ExpGrowth.le_expGrowthInf_iff, ExpGrowth.expGrowthSup_comp_le, ExpGrowth.frequently_le_exp, LinearGrowth.linearGrowthInf_eventually_monotone, ExpGrowth.frequently_exp_le, Monotone.expGrowthInf_comp_le, LinearGrowth.linearGrowthInf_iInf, LinearGrowth.linearGrowthInf_monotone, ExpGrowth.eventually_exp_le, LinearGrowth.linearGrowthSup_iSup, LinearGrowth.linearGrowthInf_comp_nonneg, LinearGrowth.le_linearGrowthInf_iff, ExpGrowth.expGrowthInf_def, LinearGrowth.linearGrowthInf_le_of_eventually_le, LinearGrowth.linearGrowthInf_le_iff, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, Monotone.linearGrowthInf_comp_mul, EReal.exp_nmul, LinearGrowth.linearGrowthInf_add_le, ExpGrowth.expGrowthSup_le_iff, EReal.natCast_div_le, Monotone.linearGrowthSup_nonneg, Monotone.linearGrowthSup_comp_mul, Monotone.le_linearGrowthSup_comp, Monotone.expGrowthSup_comp_mul, LinearGrowth.linearGrowthSup_monotone, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le, LinearGrowth.le_linearGrowthInf_comp, instCharZeroEReal, LinearGrowth.le_linearGrowthSup_iff, ExpGrowth.le_expGrowthSup_iff, EReal.natCast_le_iff, LinearGrowth.le_linearGrowthInf_add, LinearGrowth.EReal.eventually_atTop_exists_nat_between, LinearGrowth.linearGrowthInf_neg, Monotone.le_expGrowthSup_comp
instAddMonoidEReal 📖	CompOp	3 math math: EReal.nsmul_eq_mul, EReal.coe_nsmul, EReal.coe_ennreal_nsmul
instBotEReal 📖	CompOp	89 math math: EReal.continuousAt_add_coe_bot, EReal.exp_bot, EReal.bot_mul_coe_of_neg, ENNReal.log_eq_bot_iff, EReal.sub_top, EReal.bot_mul_coe_of_pos, EReal.forall, EReal.top_div_of_neg_ne_bot, EReal.neg_eq_top_iff, LinearGrowth.linearGrowthInf_bot, EReal.continuousAt_add_bot_bot, EReal.image_coe_Iio, LinearGrowth.linearGrowthSup_bot, EReal.bot_div_of_neg_ne_bot, EReal.bot_add, EReal.nhds_bot_basis, EReal.canLift, EReal.bot_lt_coe, EReal.bot_lt_add_iff, EReal.tendsto_toReal_atBot, EReal.mem_nhds_bot_iff, EReal.add_bot, EReal.top_sub_bot, Dynamics.netEntropyEntourage_empty, EReal.range_coe_eq_Ioo, EReal.image_coe_Iic, EReal.mul_top_of_neg, EReal.bot_sub, EReal.bot_mul_bot, EReal.eq_bot_iff_forall_lt, EReal.range_coe, EReal.continuousAt_add_bot_coe, EReal.continuousOn_toReal, ExpGrowth.expGrowthSup_zero, EReal.preimage_coe_Ioi_bot, EReal.bot_lt_zero, EReal.sign_bot, EReal.bot_lt_inv, EReal.bot_lt_coe_ennreal, EReal.toReal_image_Ioo_bot_zero, EReal.neg_eq_bot_iff, EReal.zero_lt_exp_iff, EReal.tendsto_exp_nhds_bot_nhds_zero, EReal.preimage_coe_Ioo_bot, EReal.bot_mul_top, EReal.tendsto_coe_nhds_bot_iff, EReal.tendsto_coe_atBot, EReal.exists, EReal.toReal_bot, EReal.top_mul_bot, EReal.sub_bot, EReal.bot_mul_of_pos, EReal.preimage_coe_Ioo_bot_top, EReal.toENNReal_bot, EReal.bot_div_of_pos_ne_top, EReal.mul_bot_of_pos, EReal.mul_eq_bot, EReal.top_mul_of_neg, EReal.nhds_bot', EReal.inv_bot, ENNReal.log_zero, EReal.nhds_bot, Dynamics.netEntropyInfEntourage_empty, Dynamics.coverEntropyInf_empty, EReal.coe_mul_bot_of_neg, ENNReal.bot_lt_log_iff, EReal.toReal_eq_zero_iff, EReal.preimage_coe_Ioc_bot, EReal.coe_sub_bot, EReal.coe_mul_bot_of_pos, EReal.exp_eq_zero_iff, EReal.abs_bot, EReal.mul_bot_of_neg, EReal.bot_mul_of_neg, ExpGrowth.expGrowthInf_zero, Dynamics.coverEntropyEntourage_empty, Dynamics.coverEntropy_empty, Dynamics.coverEntropyInfEntourage_empty, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, EReal.add_eq_bot_iff, EReal.mul_eq_top, EReal.neg_top, EReal.nhdsWithin_bot, EReal.coe_mul_top_of_neg, EReal.div_bot, EReal.neg_bot, EReal.tendsto_nhds_bot_iff_real, ENNReal.log_ofReal, EReal.top_mul_coe_of_neg
instCompleteLinearOrderEReal 📖	CompOp	81 math math: LinearGrowth.linearGrowthSup_zero, LinearGrowth.linearGrowthSup_top, LinearGrowth.linearGrowthInf_add_le', LinearGrowth.le_linearGrowthSup_add, LinearGrowth.linearGrowthSup_add_le, LinearGrowth.le_linearGrowthSup_add', ExpGrowth.expGrowthSup_add, LinearGrowth.linearGrowthInf_bot, LinearGrowth.linearGrowthSup_bot, LinearGrowth.linearGrowthInf_biInf, ExpGrowth.expGrowthSup_def, Eventually.le_linearGrowthInf, Dynamics.coverEntropyEntourage_union, LinearGrowth.linearGrowthInf_top, EReal.limsup_neg, LinearGrowth.linearGrowthInf_const_mul_self, Dynamics.coverEntropy_union, LinearGrowth.linearGrowthInf_zero, Eventually.linearGrowthSup_le, LinearGrowth.linearGrowthSup_le_of_eventually_le, EReal.min_neg_neg, LinearGrowth.linearGrowthSup_biSup, EReal.le_liminf_add, LinearGrowth.linearGrowthSup_inv, LinearGrowth.linearGrowthInf_const, EReal.liminf_add_le, LinearGrowth.linearGrowthSup_le_iff, ExpGrowth.le_expGrowthInf_comp, LinearGrowth.linearGrowthSup_const_mul_self, LinearGrowth.linearGrowthSup_sup, LinearGrowth.linearGrowthInf_inf, EReal.coe_toENNReal_eq_max, LinearGrowth.linearGrowthSup_eventually_monotone, LinearGrowth.linearGrowthSup_const, LSeries.abscissaOfAbsConv_binop_le, LSeries.abscissaOfAbsConv_add_le, LinearGrowth.linearGrowthInf_natCast_nonneg, ExpGrowth.expGrowthInf_inf, EReal.le_limsup_mul, EReal.limsup_mul_le, LinearGrowth.linearGrowthSup_comp_nonneg, EReal.le_liminf_mul, ExpGrowth.le_expGrowthInf_add, LSeries.abscissaOfAbsConv_convolution_le, Monotone.linearGrowthInf_nonneg, ExpGrowth.expGrowthSup_comp_le, EReal.liminf_neg, LinearGrowth.linearGrowthInf_eventually_monotone, EReal.liminf_mul_le, EReal.max_neg_neg, Monotone.expGrowthInf_comp_le, LinearGrowth.linearGrowthInf_iInf, LinearGrowth.linearGrowthInf_monotone, LinearGrowth.linearGrowthSup_iSup, LinearGrowth.linearGrowthInf_comp_nonneg, LinearGrowth.le_linearGrowthInf_iff, ExpGrowth.expGrowthInf_def, LinearGrowth.linearGrowthInf_le_of_eventually_le, LinearGrowth.linearGrowthInf_le_iff, EReal.le_limsup_add, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, Monotone.linearGrowthInf_comp_mul, LSeries.abscissaOfAbsConv_sub_le, LinearGrowth.linearGrowthInf_add_le, Frequently.linearGrowthInf_le, Monotone.linearGrowthInf_comp, Monotone.linearGrowthSup_nonneg, Monotone.linearGrowthSup_comp_mul, Monotone.le_linearGrowthSup_comp, ExpGrowth.expGrowthSup_sup, Monotone.linearGrowthSup_comp, LinearGrowth.linearGrowthSup_monotone, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le, LinearGrowth.le_linearGrowthInf_comp, LinearGrowth.le_linearGrowthSup_iff, LinearGrowth.le_linearGrowthInf_add, EReal.limsup_add_le, Frequently.le_linearGrowthSup, LinearGrowth.linearGrowthInf_neg, Monotone.le_expGrowthSup_comp
instInfSetEReal 📖	CompOp	5 math math: LinearGrowth.linearGrowthInf_biInf, EReal.add_iInf_le_iInf_add, ExpGrowth.expGrowthInf_iInf, LinearGrowth.linearGrowthInf_iInf, ExpGrowth.expGrowthInf_biInf
instLinearOrderEReal 📖	CompOp	—
instNontrivialEReal 📖	CompOp	—
instOneEReal 📖	CompOp	22 math math: LSeries.abscissaOfAbsConv_one, ArithmeticFunction.abscissaOfAbsConv_zeta, LSeries.abscissaOfAbsConv_le_of_le_const, EReal.abs_mul_sign, ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, EReal.one_mul, LSeries.abscissaOfAbsConv_le_one_of_isBigO_one, EReal.coe_coe_sign, DirichletCharacter.absicssaOfAbsConv_eq_one, EReal.div_self, EReal.coe_ennreal_eq_one, LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow, EReal.toReal_one, EReal.coe_one, EReal.sign_mul_inv_abs, EReal.coe_eq_one, EReal.sign_mul_abs, EReal.coe_ennreal_one, instZeroLEOneClassEReal, EReal.sign_mul_inv_abs', LSeries.abscissaOfAbsConv_le_of_isBigO_rpow, ArithmeticFunction.abscissaOfAbsConv_moebius
instPartialOrderEReal 📖	CompOp	274 math math: EReal.nhds_top_basis, Dynamics.netEntropyEntourage_monotone, Dynamics.coverEntropyInfEntourage_le_netEntropyInfEntourage, Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage, EReal.one_lt_exp_iff, EReal.inv_strictAntiOn, Complex.isOpen_re_lt_EReal, EReal.coe_le_coe_iff, Dynamics.coverEntropyInfEntourage_antitone, EReal.image_coe_Icc, ENNReal.log_lt_log_iff, Monotone.expGrowthSup_nonneg, EReal.coe_ennreal_le_coe_ennreal_iff, EReal.sub_nonneg, EReal.neg_nonneg, LinearGrowth.linearGrowthInf_add_le', LinearGrowth.le_linearGrowthSup_add, EReal.mul_nonpos_iff, EReal.toENNReal_eq_zero_iff, ENNReal.log_le_log_iff, LinearGrowth.linearGrowthSup_add_le, EReal.image_coe_Ioc, EReal.exp_strictMono, ExpGrowth.expGrowthInf_of_eventually_ge, ENNReal.log_lt_zero_iff, LSeries_injOn, EReal.neg_strictAnti, Dynamics.coverEntropy_iUnion_le, EReal.addLECancellable_coe, ExpGrowth.expGrowthInf_le_iff, EReal.image_coe_Ico, LSeriesSummable.abscissaOfAbsConv_le, EReal.neg_lt_comm, EReal.toENNReal_pos_iff, EReal.sign_eq_and_abs_eq_iff_eq, LinearGrowth.le_linearGrowthSup_add', EReal.preimage_coe_Ioi, Dynamics.netEntropyEntourage_le_coverEntropyEntourage, EReal.instPosMulMono, EReal.expOrderIso_symm, EReal.image_coe_Iio, EReal.le_coe_toReal, ExpGrowth.expGrowthInf_eventually_monotone, EReal.iSup_add_le_add_iSup, EReal.coe_nonpos, EReal.add_lt_top, EReal.neg_le_neg_iff, EReal.preimage_coe_Ioo, Dynamics.coverEntropy_monotone, ENNReal.log_strictMono, ExpGrowth.expGrowthInf_mul_le, EReal.nhds_bot_basis, LSeries_deriv_eqOn, LSeries.abscissaOfAbsConv_le_of_le_const, EReal.one_le_exp_iff, LSeries_analyticOnNhd, Dynamics.netEntropyEntourage_antitone, EReal.exists_nat_ge_mul, EReal.nhds_top', EReal.bot_lt_coe, EReal.abs_mul_sign, ArithmeticFunction.vonMangoldt.abscissaOfAbsConv_residueClass_le_one, EReal.preimage_coe_Ioo_top, EReal.bot_lt_add_iff, EReal.instMulPosMono, Dynamics.coverEntropyEntourage_le_netEntropyEntourage, ExpGrowth.expGrowthInf_comp_nonneg, EReal.mem_nhds_bot_iff, EReal.range_coe_ennreal, EReal.range_coe_eq_Ioo, ExpGrowth.expGrowthInf_le_expGrowthSup_of_frequently_le, EReal.image_coe_Iic, Dynamics.coverEntropyInfEntourage_le_coverEntropyInf, Dynamics.netEntropyInfEntourage_nonneg, EReal.instCanLiftENNRealToERealLeOfNat, ENNReal.log_le_log, Dynamics.netEntropyInfEntourage_le_netEntropyEntourage, LSeries.abscissaOfAbsConv_le_one_of_isBigO_one, Dynamics.coverEntropyInfEntourage_le_coverEntropyEntourage, ExpGrowth.expGrowthInf_monotone, Dynamics.coverEntropyEntourage_image_le, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, EReal.preimage_coe_Icc, EReal.sign_mul, ENNReal.zero_lt_log_iff, Dynamics.coverEntropyInf_image_le_of_uniformContinuous, EReal.exp_lt_exp_iff, EReal.sign_coe, EReal.le_liminf_add, ENNReal.logOrderIso_symm, EReal.exp_monotone, EReal.coe_le_coe, EReal.mul_ne_top, ENNReal.log_monotone, EReal.liminf_add_le, LinearGrowth.linearGrowthSup_le_iff, ExpGrowth.le_expGrowthInf_comp, EReal.ge_of_forall_gt_iff_ge, Dynamics.le_coverEntropyEntourage_image, EReal.eq_bot_iff_forall_lt, Dynamics.coverEntropyEntourage_monotone, EReal.mul_ne_bot, EReal.mul_nonneg_iff, Dynamics.coverEntropy_antitone, EReal.sub_lt_iff, ExpGrowth.expGrowthInf_le_of_eventually_le, EReal.preimage_coe_Ici, EReal.image_coe_Ioo, EReal.natCast_lt_iff, Dynamics.coverEntropyInf_monotone, EReal.mul_neg_iff, Frequently.expGrowthInf_le, ExpGrowth.expGrowthSup_of_eventually_ge, EReal.preimage_coe_Ioi_bot, EReal.neg_lt_zero, EReal.bot_lt_zero, EReal.preimage_coe_Ioc, Dynamics.netEntropyInfEntourage_monotone, EReal.image_coe_Ici, EReal.coe_neg', Dynamics.coverEntropyInf_nonneg, Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div, Dynamics.coverEntropyEntourage_finite_of_isCompact_invariant, LSeries.abscissaOfAbsConv_binop_le, EReal.sign_bot, EReal.bot_lt_inv, LSeries.abscissaOfAbsConv_add_le, ExpGrowth.expGrowthSup_mul_le, LinearGrowth.linearGrowthInf_natCast_nonneg, Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariant, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable', EReal.exp_le_one_iff, EReal.sub_nonpos, EReal.le_neg, EReal.bot_lt_coe_ennreal, Dynamics.coverEntropyInf_antitone, Dynamics.coverEntropyEntourage_le_log_coverMincard_div, EReal.add_iInf_le_iInf_add, EReal.neg_le_zero, EReal.coe_nonneg, ExpGrowth.le_expGrowthInf_add, EReal.toReal_image_Ioo_bot_zero, LSeries.abscissaOfAbsConv_convolution_le, EReal.zero_lt_exp_iff, EReal.preimage_coe_Ioo_bot, ENNReal.log_lt_top_iff, ExpGrowth.le_expGrowthInf_iff, ExpGrowth.expGrowthSup_comp_le, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, EReal.sub_self_le_zero, Frequently.le_expGrowthSup, EReal.coe_strictMono, EReal.coe_ennreal_lt_coe_ennreal_iff, Dynamics.coverEntropy_image_le_of_uniformContinuous, ExpGrowth.expGrowthSup_comp_nonneg, ENNReal.log_le_zero_iff, EReal.preimage_coe_Ico_top, LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow, EReal.sub_neg, Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage, Complex.isOpen_im_gt_EReal, ExpGrowth.expGrowthSup_eventually_monotone, LSeries_differentiableOn, Monotone.expGrowthInf_comp_le, Dynamics.coverEntropy_nonneg, Dynamics.coverEntropyEntourage_antitone, EReal.sign_top, EReal.preimage_coe_Iio, EReal.preimage_coe_Ioo_bot_top, EReal.lt_sub_iff_add_lt, Monotone.expGrowthInf_nonneg, ENNReal.zero_le_log_iff, EReal.instMulPosReflectLT, EReal.neg_pos, EReal.coe_pos, EReal.le_iff_sign, EReal.mul_eq_bot, EReal.le_of_forall_lt_iff_le, Eventually.le_expGrowthInf, EReal.preimage_coe_Iio_top, Dynamics.coverEntropy_biUnion_le, EReal.nhds_bot', Complex.isOpen_im_lt_EReal, Dynamics.coverEntropyEntourage_nonneg, Dynamics.netEntropyInfEntourage_le_coverEntropyInf, LinearGrowth.le_linearGrowthInf_iff, EReal.tendsto_nhds_top_iff_real, EReal.nhds_bot, ExpGrowth.le_expGrowthSup_mul', Dynamics.coverEntropyInfEntourage_image_le, LSeries_analyticOn, EReal.lt_neg_comm, EReal.exp_lt_one_iff, EReal.lowerSemicontinuous_add, EReal.toReal_image_Ioo_zero_top, EReal.inv_lt_top, Dynamics.coverEntropyInfEntourage_closure, ExpGrowth.expGrowthInf_mul_le', LinearGrowth.linearGrowthInf_le_iff, EReal.le_limsup_add, Dynamics.coverEntropyEntourage_closure, Dynamics.coverEntropyInf_iUnion_le, EReal.preimage_coe_Iic, EReal.toENNReal_ne_zero_iff, LSeries.abscissaOfAbsConv_sub_le, EReal.coe_lt_coe, EReal.exp_lt_top_iff, EReal.expOrderIso_apply, ENNReal.bot_lt_log_iff, EReal.sign_mul_inv_abs, Dynamics.netEntropyEntourage_nonneg, EReal.coe_ennreal_strictMono, EReal.lt_iff_exists_rat_btwn, EReal.preimage_coe_Ioc_bot, LinearGrowth.linearGrowthInf_add_le, Dynamics.coverEntropyInf_biUnion_le, ExpGrowth.expGrowthSup_le_iff, EReal.sign_mul_abs, EReal.sub_pos, Dynamics.coverEntropyEntourage_le_coverEntropy, EReal.sub_le_iff_le_add, EReal.natCast_div_le, EReal.preimage_coe_Ico, EReal.nhds_top, instIsOrderedAddMonoidEReal, Dynamics.netEntropyEntourage_le_coverEntropy, Dynamics.coverEntropyInf_image_le_of_uniformContinuousOn_invariant, EReal.mul_pos_iff, EReal.sign_neg, Dynamics.le_coverEntropyInfEntourage_image, EReal.zero_lt_top, Eventually.expGrowthSup_le, ExpGrowth.expGrowthSup_le_of_eventually_le, Dynamics.netEntropyInfEntourage_antitone, EReal.neg_le, ENNReal.log_lt_log, EReal.coe_ennreal_nonneg, EReal.coe_nnreal_lt_top, EReal.coe_ennreal_pos_iff_ne_zero, instZeroLEOneClassEReal, Dynamics.coverEntropyInfEntourage_nonneg, ExpGrowth.le_expGrowthSup_mul, MeasureTheory.exists_upperSemicontinuous_lt_integral_gt, EReal.image_coe_Ioi, EReal.le_sub_iff_add_le, instDenselyOrderedEReal, EReal.mul_eq_top, ExpGrowth.le_expGrowthInf_mul, LinearGrowth.le_linearGrowthSup_iff, ExpGrowth.le_expGrowthSup_iff, ExpGrowth.expGrowthInf_le_expGrowthSup, EReal.exp_le_exp_iff, EReal.natCast_le_iff, EReal.eq_top_iff_forall_lt, Complex.isOpen_re_gt_EReal, EReal.sign_mul_inv_abs', ENNReal.logOrderIso_apply, ExpGrowth.expGrowthSup_monotone, Dynamics.coverEntropyInfEntourage_monotone, LinearGrowth.le_linearGrowthInf_add, EReal.coe_toReal_le, EReal.coe_lt_coe_iff, EReal.mem_nhds_top_iff, Dynamics.coverEntropyInf_le_coverEntropy, EReal.limsup_add_le, EReal.coe_lt_top, EReal.instOrderTopology, EReal.neg_lt_neg_iff, EReal.coe_ennreal_pos, LSeries.abscissaOfAbsConv_le_of_isBigO_rpow, EReal.tendsto_nhds_bot_iff_real, EReal.instPosMulReflectLT, EReal.lt_iff_exists_real_btwn, Monotone.le_expGrowthSup_comp
instSupSetEReal 📖	CompOp	18 math math: Dynamics.coverEntropy_iUnion_le, EReal.iSup_add_le_add_iSup, ExpGrowth.expGrowthSup_sum, ExpGrowth.expGrowthSup_biSup, Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage, LinearGrowth.linearGrowthSup_biSup, Dynamics.coverEntropy_biUnion_finset, Dynamics.coverEntropy_iUnion_of_finite, Dynamics.coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, LinearGrowth.linearGrowthSup_iSup, Dynamics.coverEntropy_eq_iSup_basis, Dynamics.coverEntropy_eq_iSup_basis_netEntropyEntourage, Dynamics.coverEntropy_biUnion_le, Dynamics.coverEntropy_eq_iSup_netEntropyEntourage, Dynamics.coverEntropyInf_iUnion_le, Dynamics.coverEntropyInf_biUnion_le, ExpGrowth.expGrowthSup_iSup, Dynamics.coverEntropyInf_eq_iSup_basis
instZeroEReal 📖	CompOp	110 math math: LinearGrowth.linearGrowthSup_zero, EReal.one_lt_exp_iff, EReal.inv_strictAntiOn, Monotone.expGrowthSup_nonneg, EReal.sub_nonneg, EReal.neg_nonneg, EReal.mul_nonpos_iff, EReal.toENNReal_eq_zero_iff, ENNReal.log_lt_zero_iff, EReal.toENNReal_pos_iff, EReal.sign_eq_and_abs_eq_iff_eq, Dynamics.netEntropyInfEntourage_univ, Dynamics.coverEntropyInfEntourage_univ, EReal.abs_eq_zero_iff, EReal.instPosMulMono, Dynamics.coverEntropyEntourage_univ, EReal.sub_self, EReal.coe_nonpos, EReal.tendsto_exp_nhds_zero_nhds_one, EReal.one_le_exp_iff, EReal.abs_mul_sign, EReal.toReal_zero, EReal.instMulPosMono, ExpGrowth.expGrowthInf_comp_nonneg, EReal.range_coe_ennreal, LinearGrowth.linearGrowthInf_zero, EReal.neg_eq_zero_iff, Dynamics.netEntropyInfEntourage_nonneg, EReal.instCanLiftENNRealToERealLeOfNat, EReal.coe_ennreal_zero, EReal.sign_mul, ENNReal.zero_lt_log_iff, ENNReal.log_eq_one_iff, EReal.sign_coe, ExpGrowth.expGrowthSup_const, LinearGrowth.linearGrowthInf_const, EReal.mul_ne_top, EReal.coe_zero, EReal.tendsto_const_div_atTop_nhds_zero_nat, EReal.mul_ne_bot, EReal.mul_nonneg_iff, EReal.mul_neg_iff, EReal.coe_coe_sign, EReal.neg_lt_zero, EReal.coe_toENNReal_eq_max, EReal.bot_lt_zero, EReal.div_zero, EReal.coe_neg', Dynamics.coverEntropyInf_nonneg, LinearGrowth.linearGrowthSup_const, EReal.coe_ennreal_eq_zero, EReal.sign_bot, LinearGrowth.linearGrowthInf_natCast_nonneg, LinearGrowth.linearGrowthSup_comp_nonneg, EReal.exp_le_one_iff, EReal.sub_nonpos, EReal.neg_le_zero, EReal.coe_nonneg, EReal.toReal_image_Ioo_bot_zero, Monotone.linearGrowthInf_nonneg, EReal.abs_zero, EReal.sub_self_le_zero, ExpGrowth.expGrowthSup_comp_nonneg, ENNReal.log_le_zero_iff, EReal.sub_neg, EReal.inv_top, Dynamics.coverEntropy_nonneg, EReal.instNoZeroDivisors, EReal.sign_top, EReal.toENNReal_zero, Monotone.expGrowthInf_nonneg, EReal.exp_zero, LinearGrowth.linearGrowthInf_comp_nonneg, ENNReal.zero_le_log_iff, EReal.instMulPosReflectLT, EReal.div_top, EReal.neg_pos, EReal.coe_pos, EReal.le_iff_sign, EReal.mul_eq_bot, ENNReal.log_one, EReal.coe_eq_zero, EReal.inv_bot, Dynamics.coverEntropyEntourage_nonneg, EReal.exp_lt_one_iff, EReal.toReal_image_Ioo_zero_top, EReal.toENNReal_ne_zero_iff, ExpGrowth.expGrowthInf_const, EReal.zero_div, EReal.toReal_eq_zero_iff, EReal.sign_mul_inv_abs, Dynamics.netEntropyEntourage_nonneg, EReal.sign_mul_abs, EReal.sub_pos, EReal.mul_pos_iff, Monotone.linearGrowthSup_nonneg, EReal.sign_neg, EReal.zero_lt_top, EReal.zero_mul, EReal.coe_ennreal_nonneg, EReal.coe_ennreal_pos_iff_ne_zero, instZeroLEOneClassEReal, Dynamics.coverEntropyInfEntourage_nonneg, EReal.mul_eq_top, EReal.sign_mul_inv_abs', EReal.div_bot, EReal.inv_zero, Dynamics.netEntropyEntourage_univ, EReal.coe_ennreal_pos, EReal.instPosMulReflectLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCharZeroEReal 📖	mathematical	—	CharZero EReal AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	WithBot.charZero WithTop.charZero IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
instDenselyOrderedEReal 📖	mathematical	—	DenselyOrdered EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal	—	WithBot.denselyOrdered WithTop.denselyOrdered LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial WithTop.noMinOrder instNoMinOrderOfNontrivial
instIsOrderedAddMonoidEReal 📖	mathematical	—	IsOrderedAddMonoid EReal instAddCommMonoidEReal instPartialOrderEReal	—	WithBot.isOrderedAddMonoid WithTop.isOrderedAddMonoid Real.instIsOrderedAddMonoid
instZeroLEOneClassEReal 📖	mathematical	—	ZeroLEOneClass EReal instZeroEReal instOneEReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal	—	WithBot.zeroLEOneClass WithTop.zeroLEOneClass Real.instZeroLEOneClass

---

← Back to Index