UniformConvergence

📁 Source: Mathlib/Topology/Algebra/UniformConvergence.lean

Statistics

Metric	Count
Definitions `instAddCommGroupUniformFun`, `instAddCommGroupUniformOnFun`, `instAddCommMonoidUniformFun`, `instAddCommMonoidUniformOnFun`, `instAddGroupUniformFun`, `instAddGroupUniformOnFun`, `instAddMonoidUniformFun`, `instAddMonoidUniformOnFun`, `instAddUniformFun`, `instAddUniformOnFun`, `instCommGroupUniformFun`, `instCommGroupUniformOnFun`, `instCommMonoidUniformFun`, `instCommMonoidUniformOnFun`, `instDistribMulActionUniformFun`, `instDistribMulActionUniformOnFun`, `instDivUniformFun`, `instDivUniformOnFun`, `instGroupUniformFun`, `instGroupUniformOnFun`, `instInvUniformFun`, `instInvUniformOnFun`, `instModuleUniformFun`, `instModuleUniformOnFun`, `instMonoidUniformFun`, `instMonoidUniformOnFun`, `instMulActionUniformFun`, `instMulActionUniformOnFun`, `instMulUniformFun`, `instMulUniformOnFun`, `instNegUniformFun`, `instNegUniformOnFun`, `instOneUniformFun`, `instOneUniformOnFun`, `instSMulUniformFun`, `instSMulUniformOnFun`, `instSubUniformFun`, `instSubUniformOnFun`, `instZeroUniformFun`, `instZeroUniformOnFun`	40
Theorems `hasBasis_nhds_one`, `hasBasis_nhds_one_of_basis`, `hasBasis_nhds_zero`, `hasBasis_nhds_zero_of_basis`, `ofFun_add`, `ofFun_div`, `ofFun_inv`, `ofFun_mul`, `ofFun_neg`, `ofFun_one`, `ofFun_prod`, `ofFun_smul`, `ofFun_sub`, `ofFun_sum`, `ofFun_zero`, `toFun_add`, `toFun_div`, `toFun_inv`, `toFun_mul`, `toFun_neg`, `toFun_one`, `toFun_prod`, `toFun_smul`, `toFun_sub`, `toFun_sum`, `toFun_zero`, `uniformContinuousConstSMul`, `uniformContinuousConstSMul`, `hasBasis_nhds_one`, `hasBasis_nhds_one_of_basis`, `hasBasis_nhds_zero`, `hasBasis_nhds_zero_of_basis`, `ofFun_add`, `ofFun_div`, `ofFun_inv`, `ofFun_mul`, `ofFun_neg`, `ofFun_prod`, `ofFun_smul`, `ofFun_sub`, `ofFun_sum`, `one_apply`, `toFun_add`, `toFun_div`, `toFun_inv`, `toFun_mul`, `toFun_neg`, `toFun_one`, `toFun_prod`, `toFun_smul`, `toFun_sub`, `toFun_sum`, `toFun_zero`, `zero_apply`, `instIsScalarTowerUniformFun`, `instIsScalarTowerUniformOnFun`, `instIsUniformAddGroupUniformFun`, `instIsUniformAddGroupUniformOnFun`, `instIsUniformGroupUniformFun`, `instIsUniformGroupUniformOnFun`, `instSMulCommClassUniformFun`, `instSMulCommClassUniformOnFun`	62
Total	102

UniformFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_nhds_one` 📖	mathematical	—	`Filter.HasBasis` `UniformFun` `Set` `nhds` `topologicalSpace` `instOneUniformFun` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Filter` `Filter.instMembership` `UniformSpace.toTopologicalSpace` `setOf`	—	`hasBasis_nhds_one_of_basis` `Filter.basis_sets`
`hasBasis_nhds_one_of_basis` 📖	mathematical	`Filter.HasBasis` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`UniformFun` `topologicalSpace` `instOneUniformFun` `setOf`	—	`div_one` `hasBasis_nhds_of_basis` `Filter.HasBasis.uniformity_of_nhds_one`
`hasBasis_nhds_zero` 📖	mathematical	—	`Filter.HasBasis` `UniformFun` `Set` `nhds` `topologicalSpace` `instZeroUniformFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Filter` `Filter.instMembership` `UniformSpace.toTopologicalSpace` `setOf`	—	`hasBasis_nhds_zero_of_basis` `Filter.basis_sets`
`hasBasis_nhds_zero_of_basis` 📖	mathematical	`Filter.HasBasis` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`UniformFun` `topologicalSpace` `instZeroUniformFun` `setOf`	—	`mem_gen` `sub_zero` `hasBasis_nhds_of_basis` `Filter.HasBasis.uniformity_of_nhds_zero`
`ofFun_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instAdd` `instAddUniformFun`	—	—
`ofFun_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instDiv` `instDivUniformFun`	—	—
`ofFun_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instInv` `instInvUniformFun`	—	—
`ofFun_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instMul` `instMulUniformFun`	—	—
`ofFun_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instNeg` `instNegUniformFun`	—	—
`ofFun_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instOne` `instOneUniformFun`	—	—
`ofFun_prod` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Finset.prod` `Pi.commMonoid` `instCommMonoidUniformFun`	—	—
`ofFun_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Function.hasSMul` `instSMulUniformFun`	—	—
`ofFun_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instSub` `instSubUniformFun`	—	—
`ofFun_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Finset.sum` `Pi.addCommMonoid` `instAddCommMonoidUniformFun`	—	—
`ofFun_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instZero` `instZeroUniformFun`	—	—
`toFun_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instAddUniformFun` `Pi.instAdd`	—	—
`toFun_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instDivUniformFun` `Pi.instDiv`	—	—
`toFun_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instInvUniformFun` `Pi.instInv`	—	—
`toFun_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instMulUniformFun` `Pi.instMul`	—	—
`toFun_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instNegUniformFun` `Pi.instNeg`	—	—
`toFun_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instOneUniformFun` `Pi.instOne`	—	—
`toFun_prod` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `Finset.prod` `instCommMonoidUniformFun` `Pi.commMonoid`	—	—
`toFun_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instSMulUniformFun` `Function.hasSMul`	—	—
`toFun_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instSubUniformFun` `Pi.instSub`	—	—
`toFun_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `Finset.sum` `instAddCommMonoidUniformFun` `Pi.addCommMonoid`	—	—
`toFun_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instZeroUniformFun` `Pi.instZero`	—	—
`uniformContinuousConstSMul` 📖	mathematical	—	`UniformContinuousConstSMul` `UniformFun` `uniformSpace` `instSMulUniformFun`	—	`postcomp_uniformContinuous` `UniformContinuousConstSMul.uniformContinuous_const_smul`

UniformFunOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformContinuousConstSMul` 📖	mathematical	—	`UniformContinuousConstSMul` `UniformOnFun` `UniformOnFun.uniformSpace` `instSMulUniformOnFun`	—	`UniformOnFun.postcomp_uniformContinuous` `UniformContinuousConstSMul.uniformContinuous_const_smul`

UniformOnFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_nhds_one` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset`	`Filter.HasBasis` `UniformOnFun` `nhds` `topologicalSpace` `instOneUniformOnFun` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Set.instMembership` `Filter` `Filter.instMembership` `UniformSpace.toTopologicalSpace` `setOf`	—	`hasBasis_nhds_one_of_basis` `Filter.basis_sets`
`hasBasis_nhds_one_of_basis` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset` `Filter.HasBasis` `nhds` `UniformSpace.toTopologicalSpace` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`UniformOnFun` `topologicalSpace` `instOneUniformOnFun` `Set.instMembership` `setOf`	—	`div_one` `hasBasis_nhds_of_basis` `Filter.HasBasis.uniformity_of_nhds_one_swapped`
`hasBasis_nhds_zero` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset`	`Filter.HasBasis` `UniformOnFun` `nhds` `topologicalSpace` `instZeroUniformOnFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set.instMembership` `Filter` `Filter.instMembership` `UniformSpace.toTopologicalSpace` `setOf`	—	`hasBasis_nhds_zero_of_basis` `Filter.basis_sets`
`hasBasis_nhds_zero_of_basis` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset` `Filter.HasBasis` `nhds` `UniformSpace.toTopologicalSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`UniformOnFun` `topologicalSpace` `instZeroUniformOnFun` `Set.instMembership` `setOf`	—	`sub_zero` `hasBasis_nhds_of_basis` `Filter.HasBasis.uniformity_of_nhds_zero_swapped`
`ofFun_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instAdd` `instAddUniformOnFun`	—	—
`ofFun_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instDiv` `instDivUniformOnFun`	—	—
`ofFun_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instInv` `instInvUniformOnFun`	—	—
`ofFun_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instMul` `instMulUniformOnFun`	—	—
`ofFun_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instNeg` `instNegUniformOnFun`	—	—
`ofFun_prod` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Finset.prod` `Pi.commMonoid` `instCommMonoidUniformOnFun`	—	—
`ofFun_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Function.hasSMul` `instSMulUniformOnFun`	—	—
`ofFun_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instSub` `instSubUniformOnFun`	—	—
`ofFun_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Finset.sum` `Pi.addCommMonoid` `instAddCommMonoidUniformOnFun`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instOne` `instOneUniformOnFun`	—	—
`toFun_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instAddUniformOnFun` `Pi.instAdd`	—	—
`toFun_div` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instDivUniformOnFun` `Pi.instDiv`	—	—
`toFun_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instInvUniformOnFun` `Pi.instInv`	—	—
`toFun_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instMulUniformOnFun` `Pi.instMul`	—	—
`toFun_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instNegUniformOnFun` `Pi.instNeg`	—	—
`toFun_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instOneUniformOnFun` `Pi.instOne`	—	—
`toFun_prod` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `Finset.prod` `instCommMonoidUniformOnFun` `Pi.commMonoid`	—	—
`toFun_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instSMulUniformOnFun` `Function.hasSMul`	—	—
`toFun_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instSubUniformOnFun` `Pi.instSub`	—	—
`toFun_sum` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `Finset.sum` `instAddCommMonoidUniformOnFun` `Pi.addCommMonoid`	—	—
`toFun_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instZeroUniformOnFun` `Pi.instZero`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `Pi.instZero` `instZeroUniformOnFun`	—	—

(root)

Definitions

Name	Category	Theorems
`instAddCommGroupUniformFun` 📖	CompOp	—
`instAddCommGroupUniformOnFun` 📖	CompOp	—
`instAddCommMonoidUniformFun` 📖	CompOp	2 math math: `UniformFun.ofFun_sum`, `UniformFun.toFun_sum`
`instAddCommMonoidUniformOnFun` 📖	CompOp	3 math math: `UniformOnFun.ofFun_sum`, `UniformOnFun.toFun_sum`, `UniformOnFun.continuousSMul_submodule_of_image_bounded`
`instAddGroupUniformFun` 📖	CompOp	1 math math: `instIsUniformAddGroupUniformFun`
`instAddGroupUniformOnFun` 📖	CompOp	1 math math: `instIsUniformAddGroupUniformOnFun`
`instAddMonoidUniformFun` 📖	CompOp	—
`instAddMonoidUniformOnFun` 📖	CompOp	—
`instAddUniformFun` 📖	CompOp	2 math math: `UniformFun.toFun_add`, `UniformFun.ofFun_add`
`instAddUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.toFun_add`, `UniformOnFun.ofFun_add`
`instCommGroupUniformFun` 📖	CompOp	—
`instCommGroupUniformOnFun` 📖	CompOp	—
`instCommMonoidUniformFun` 📖	CompOp	2 math math: `UniformFun.toFun_prod`, `UniformFun.ofFun_prod`
`instCommMonoidUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.ofFun_prod`, `UniformOnFun.toFun_prod`
`instDistribMulActionUniformFun` 📖	CompOp	—
`instDistribMulActionUniformOnFun` 📖	CompOp	—
`instDivUniformFun` 📖	CompOp	2 math math: `UniformFun.ofFun_div`, `UniformFun.toFun_div`
`instDivUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.toFun_div`, `UniformOnFun.ofFun_div`
`instGroupUniformFun` 📖	CompOp	1 math math: `instIsUniformGroupUniformFun`
`instGroupUniformOnFun` 📖	CompOp	1 math math: `instIsUniformGroupUniformOnFun`
`instInvUniformFun` 📖	CompOp	2 math math: `UniformFun.toFun_inv`, `UniformFun.ofFun_inv`
`instInvUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.ofFun_inv`, `UniformOnFun.toFun_inv`
`instModuleUniformFun` 📖	CompOp	—
`instModuleUniformOnFun` 📖	CompOp	1 math math: `UniformOnFun.continuousSMul_submodule_of_image_bounded`
`instMonoidUniformFun` 📖	CompOp	—
`instMonoidUniformOnFun` 📖	CompOp	—
`instMulActionUniformFun` 📖	CompOp	—
`instMulActionUniformOnFun` 📖	CompOp	—
`instMulUniformFun` 📖	CompOp	2 math math: `UniformFun.toFun_mul`, `UniformFun.ofFun_mul`
`instMulUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.ofFun_mul`, `UniformOnFun.toFun_mul`
`instNegUniformFun` 📖	CompOp	2 math math: `UniformFun.ofFun_neg`, `UniformFun.toFun_neg`
`instNegUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.toFun_neg`, `UniformOnFun.ofFun_neg`
`instOneUniformFun` 📖	CompOp	4 math math: `UniformFun.ofFun_one`, `UniformFun.toFun_one`, `UniformFun.hasBasis_nhds_one_of_basis`, `UniformFun.hasBasis_nhds_one`
`instOneUniformOnFun` 📖	CompOp	4 math math: `UniformOnFun.toFun_one`, `UniformOnFun.one_apply`, `UniformOnFun.hasBasis_nhds_one_of_basis`, `UniformOnFun.hasBasis_nhds_one`
`instSMulUniformFun` 📖	CompOp	5 math math: `instIsScalarTowerUniformFun`, `UniformFun.toFun_smul`, `instSMulCommClassUniformFun`, `UniformFun.ofFun_smul`, `UniformFun.uniformContinuousConstSMul`
`instSMulUniformOnFun` 📖	CompOp	6 math math: `instSMulCommClassUniformOnFun`, `instIsScalarTowerUniformOnFun`, `UniformFunOn.uniformContinuousConstSMul`, `UniformOnFun.continuousSMul_submodule_of_image_bounded`, `UniformOnFun.toFun_smul`, `UniformOnFun.ofFun_smul`
`instSubUniformFun` 📖	CompOp	2 math math: `UniformFun.toFun_sub`, `UniformFun.ofFun_sub`
`instSubUniformOnFun` 📖	CompOp	2 math math: `UniformOnFun.ofFun_sub`, `UniformOnFun.toFun_sub`
`instZeroUniformFun` 📖	CompOp	4 math math: `UniformFun.hasBasis_nhds_zero_of_basis`, `UniformFun.hasBasis_nhds_zero`, `UniformFun.toFun_zero`, `UniformFun.ofFun_zero`
`instZeroUniformOnFun` 📖	CompOp	4 math math: `UniformOnFun.hasBasis_nhds_zero_of_basis`, `UniformOnFun.hasBasis_nhds_zero`, `UniformOnFun.zero_apply`, `UniformOnFun.toFun_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerUniformFun` 📖	mathematical	—	`IsScalarTower` `UniformFun` `instSMulUniformFun`	—	`Pi.isScalarTower`
`instIsScalarTowerUniformOnFun` 📖	mathematical	—	`IsScalarTower` `UniformOnFun` `instSMulUniformOnFun`	—	`Pi.isScalarTower`
`instIsUniformAddGroupUniformFun` 📖	mathematical	—	`IsUniformAddGroup` `UniformFun` `UniformFun.uniformSpace` `instAddGroupUniformFun`	—	`UniformContinuous.comp` `UniformFun.postcomp_uniformContinuous` `uniformContinuous_sub` `UniformEquiv.uniformContinuous`
`instIsUniformAddGroupUniformOnFun` 📖	mathematical	—	`IsUniformAddGroup` `UniformOnFun` `UniformOnFun.uniformSpace` `instAddGroupUniformOnFun`	—	`UniformContinuous.comp` `UniformOnFun.postcomp_uniformContinuous` `uniformContinuous_sub` `UniformEquiv.uniformContinuous`
`instIsUniformGroupUniformFun` 📖	mathematical	—	`IsUniformGroup` `UniformFun` `UniformFun.uniformSpace` `instGroupUniformFun`	—	`UniformContinuous.comp` `UniformFun.postcomp_uniformContinuous` `uniformContinuous_div` `UniformEquiv.uniformContinuous`
`instIsUniformGroupUniformOnFun` 📖	mathematical	—	`IsUniformGroup` `UniformOnFun` `UniformOnFun.uniformSpace` `instGroupUniformOnFun`	—	`UniformContinuous.comp` `UniformOnFun.postcomp_uniformContinuous` `uniformContinuous_div` `UniformEquiv.uniformContinuous`
`instSMulCommClassUniformFun` 📖	mathematical	—	`SMulCommClass` `UniformFun` `instSMulUniformFun`	—	`Pi.smulCommClass`
`instSMulCommClassUniformOnFun` 📖	mathematical	—	`SMulCommClass` `UniformOnFun` `instSMulUniformOnFun`	—	`Pi.smulCommClass`

---

← Back to Index