Hofer

📁 Source: Mathlib/Analysis/Hofer.lean

Statistics

Metric	Count
Definitions	0
Theorems hofer	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hofer 📖	mathematical	Real Real.instLT Real.instZero Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.pseudoMetricSpace Real.instLE	Dist.dist PseudoMetricSpace.toDist Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat div_mul_eq_mul_div le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo mul_assoc mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono PosMulStrictMono.toPosMulReflectLE mul_comm Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq div_pos PosMulReflectLE.toPosMulReflectLT div_le_self LT.lt.le one_le_pow₀ Real.instZeroLEOneClass one_le_two IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.case_strong_induction_on zero_add pow_zero div_one dist_self one_mul dist_comm dist_le_range_sum_dist Finset.sum_le_sum Finset.mem_range Finset.sum_mul Finset.sum_congr one_div inv_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' one_ne_zero NeZero.one GroupWithZero.toNontrivial mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono sum_geometric_two_le le_of_lt geom_le zero_le_two cauchySeq_of_le_geometric one_half_lt_one CompleteSpace.complete mul_nonneg tendsto_atTop_of_geom_le one_lt_two NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Filter.tendsto_add_atTop_iff_nat Filter.Tendsto.comp Continuous.continuousAt not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Function.sometimes_spec

---

← Back to Index