ZeroAndBoundedAtFilter

📁 Source: Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

Statistics

Metric	Count
Definitions BoundedAtFilter, ZeroAtFilter, boundedFilterSubalgebra, boundedFilterSubmodule, zeroAtFilterAddSubmonoid, zeroAtFilterSubmodule	6
Theorems add, mul, neg, prod, smul, add, boundedAtFilter, neg, smul, const_boundedAtFilter, zero_zeroAtFilter	11
Total	17

Filter

Definitions

Name	Category	Theorems
BoundedAtFilter 📖	MathDef	3 math math: const_boundedAtFilter, ModularFormClass.bounded_at_infty_comp_ofComplex, ZeroAtFilter.boundedAtFilter
ZeroAtFilter 📖	MathDef	3 math math: CuspFormClass.zero_at_infty_comp_ofComplex, zero_zeroAtFilter, UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex
boundedFilterSubalgebra 📖	CompOp	—
boundedFilterSubmodule 📖	CompOp	—
zeroAtFilterAddSubmonoid 📖	CompOp	—
zeroAtFilterSubmodule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_boundedAtFilter 📖	mathematical	—	BoundedAtFilter	—	Asymptotics.isBigO_const_const one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
zero_zeroAtFilter 📖	mathematical	—	ZeroAtFilter Pi.instZero	—	tendsto_const_nhds

Filter.BoundedAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Filter.BoundedAtFilter SeminormedAddCommGroup.toNorm	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	Asymptotics.IsBigO.add
mul 📖	mathematical	Filter.BoundedAtFilter SeminormedRing.toNorm	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing	—	Asymptotics.IsBigO.trans Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass mul_one Asymptotics.isBigO_refl
neg 📖	mathematical	Filter.BoundedAtFilter SeminormedAddCommGroup.toNorm	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	Asymptotics.IsBigO.neg_left
prod 📖	mathematical	Filter.BoundedAtFilter SeminormedRing.toNorm SeminormedCommRing.toSeminormedRing	Finset.prod Pi.commMonoid CommRing.toCommMonoid SeminormedCommRing.toCommRing	—	Subalgebra.prod_mem NonUnitalSeminormedRing.isBoundedSMul
smul 📖	mathematical	Filter.BoundedAtFilter SeminormedAddCommGroup.toNorm	Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	Asymptotics.IsBigO.const_smul_left

Filter.ZeroAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Filter.ZeroAtFilter AddZero.toZero AddZeroClass.toAddZero	Pi.instAdd AddZero.toAdd	—	add_zero Filter.Tendsto.add
boundedAtFilter 📖	mathematical	Filter.ZeroAtFilter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	Filter.BoundedAtFilter SeminormedAddGroup.toNorm	—	Asymptotics.IsLittleO.isBigO Asymptotics.isLittleO_one_iff NormedDivisionRing.to_normOneClass
neg 📖	mathematical	Filter.ZeroAtFilter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	Pi.instNeg NegZeroClass.toNeg	—	neg_zero Filter.Tendsto.neg
smul 📖	mathematical	Filter.ZeroAtFilter	Function.hasSMul SMulZeroClass.toSMul	—	smul_zero Filter.Tendsto.const_smul

---

← Back to Index