UniformConvergence

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

Statistics

Metric	Count
Definitions	0
Theorems continuousSMul_induced_of_range_bounded, continuousSMul_induced_of_image_bounded, continuousSMul_submodule_of_image_bounded	3
Total	3

UniformFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul_induced_of_range_bounded 📖	mathematical	Topology.IsInducing UniformFun topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformSpace.toTopologicalSpace Set.range	ContinuousSMul PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	—	Topology.IsInducing.topologicalAddGroup IsUniformAddGroup.to_topologicalAddGroup instIsUniformAddGroupUniformFun AddMonoidHom.instAddMonoidHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Topology.IsInducing.nhds_eq_comap map_zero AddMonoidHomClass.toZeroHomClass Filter.HasBasis.comap hasBasis_nhds_zero ContinuousSMul.of_basis_zero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.tendsto' ContinuousSMul.continuous_smul zero_smul Filter.HasBasis.tendsto_left_iff Filter.HasBasis.prod_nhds Filter.basis_sets Set.smul_subset_iff map_smul SemilinearMapClass.toMulActionSemiHomClass Set.mk_mem_prod ContinuousConstSMul.continuous_const_smul ContinuousSMul.continuousConstSMul smul_zero Absorbs.eventually_nhds_zero mem_of_mem_nhds

UniformOnFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul_induced_of_image_bounded 📖	mathematical	Topology.IsInducing UniformOnFun topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofFun Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformSpace.toTopologicalSpace Set.image	ContinuousSMul PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	—	topologicalSpace_eq induced_iInf iInf_congr_Prop induced_compose continuousSMul_iInf map_add SemilinearMapClass.toAddHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass UniformFun.continuousSMul_induced_of_range_bounded LinearMap.semilinearMapClass Set.image_eq_range Topology.IsInducing.eq_induced
continuousSMul_submodule_of_image_bounded 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformSpace.toTopologicalSpace Set.image	ContinuousSMul UniformOnFun Submodule instAddCommMonoidUniformOnFun instModuleUniformOnFun SetLike.instMembership Submodule.setLike Submodule.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id instSMulUniformOnFun instIsScalarTowerUniformOnFun SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid IsScalarTower.left PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace TopologicalSpace.induced topologicalSpace	—	continuousSMul_induced_of_image_bounded LinearMap.semilinearMapClass Topology.IsInducing.subtypeVal

---

← Back to Index