Documentation Verification Report

Subadditive

📁 Source: Mathlib/Analysis/Subadditive.lean

Statistics

Metric	Count
Definitions `Subadditive`, `lim`	2
Theorems `apply_mul_add_le`, `eventually_div_lt_of_div_lt`, `lim_le_div`, `tendsto_lim`	4
Total	6

Subadditive

Definitions

Name	Category	Theorems
`lim` 📖	CompOp	2 math math: `tendsto_lim`, `lim_le_div`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mul_add_le` 📖	mathematical	`Subadditive`	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `Real.instNatCast`	—	`MulZeroClass.zero_mul` `zero_add` `Nat.cast_zero` `le_refl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_add` `Nat.cast_one`
`eventually_div_lt_of_div_lt` 📖	mathematical	`Subadditive` `Real` `Real.instLT` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	`Filter.Eventually` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Eventually.atTop_of_arithmetic` `Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `tendsto_const_nhds` `Filter.Tendsto.div_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.tendsto_id` `add_zero` `IsStrictOrderedRing.toCharZero` `Filter.Tendsto.congr'` `Filter.Eventually.mono` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `add_div'` `mul_comm` `div_div_div_cancel_right₀` `Filter.Tendsto.eventually` `Filter.Tendsto.comp` `tendsto_natCast_atTop_atTop` `Real.instArchimedean` `gt_mem_nhds` `lt_of_le_of_lt` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `apply_mul_add_le` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass`
`lim_le_div` 📖	mathematical	`Subadditive` `BddBelow` `Real` `Real.instLE` `Set.range` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	`lim`	—	`lim.eq_1` `csInf_le` `BddBelow.mono` `Set.image_subset_range` `Ne.bot_lt`
`tendsto_lim` 📖	mathematical	`Subadditive` `BddBelow` `Real` `Real.instLE` `Set.range` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `lim`	—	`tendsto_order` `instOrderTopologyReal` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LT.lt.trans_le` `lim_le_div` `LT.lt.ne'` `zero_lt_one` `Nat.instZeroLEOneClass` `exists_lt_of_csInf_lt` `lim.eq_1` `Set.mem_image` `eventually_div_lt_of_div_lt`

(root)

Definitions

Name	Category	Theorems
`Subadditive` 📖	MathDef	—

---

← Back to Index