ApproximateUnit

📁 Source: Mathlib/Topology/ApproximateUnit.lean

Statistics

Metric	Count
Definitions IsApproximateUnit	1
Theorems iff_le_nhds_one, iff_neBot_and_le_nhds_one, mono, neBot, nhds_one, pure_one, tendsto_mul_left, tendsto_mul_right	8
Total	9

Filter

Definitions

Name	Category	Theorems
IsApproximateUnit 📖	CompData	5 math math: IsApproximateUnit.iff_le_nhds_one, IsIncreasingApproximateUnit.toIsApproximateUnit, IsApproximateUnit.nhds_one, IsApproximateUnit.pure_one, IsApproximateUnit.iff_neBot_and_le_nhds_one

Filter.IsApproximateUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_le_nhds_one 📖	mathematical	—	Filter.IsApproximateUnit MulOne.toMul MulOneClass.toMulOne Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds MulOne.toOne	—	—
iff_neBot_and_le_nhds_one 📖	mathematical	—	Filter.IsApproximateUnit MulOne.toMul MulOneClass.toMulOne Filter.NeBot Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds MulOne.toOne	—	neBot one_mul tendsto_mul_left mono nhds_one
mono 📖	—	Filter.IsApproximateUnit MulOne.toMul MulOneClass.toMulOne Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder	—	—	Filter.Tendsto.mono_left tendsto_mul_left tendsto_mul_right
neBot 📖	mathematical	Filter.IsApproximateUnit	Filter.NeBot	—	—
nhds_one 📖	mathematical	—	Filter.IsApproximateUnit MulOne.toMul MulOneClass.toMulOne nhds MulOne.toOne	—	mul_one Filter.Tendsto.const_mul Filter.tendsto_id one_mul Filter.Tendsto.mul_const nhds_neBot
pure_one 📖	mathematical	—	Filter.IsApproximateUnit MulOne.toMul MulOneClass.toMulOne Filter Filter.instPure MulOne.toOne	—	mul_one tendsto_pure_nhds one_mul Filter.pure_neBot
tendsto_mul_left 📖	mathematical	Filter.IsApproximateUnit	Filter.Tendsto nhds	—	—
tendsto_mul_right 📖	mathematical	Filter.IsApproximateUnit	Filter.Tendsto nhds	—	—

---

← Back to Index