MulAction

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

Statistics

Metric	Count
Definitions ContinuousSMul, ContinuousVAdd, MulAction	3
Theorems continuousVAdd_compHom, continuousVAdd, continuousVAdd, continuousVAdd, connectedSpace, continuousVAdd, smul, vadd, smul, vadd, smul, vadd, continuousConstSMul, continuous_smul, induced, op, continuousConstVAdd, continuous_vadd, op, smul, vadd, smul, smul_const, vadd, vadd_const, top_smul_nhds_zero, smul, vadd, smul_set, vadd_set, continuousSMul, continuousSMul_compHom, continuousSMul, continuousSMul, continuousVAdd, continuousSMul, univ_smul_nhds_zero, smul, vadd, continuousSMul, continuousSMul, continuousSMul, continuousVAdd, continuousSMul, continuousVAdd, continuousSMul_iInf, continuousSMul_iff_stabilizer_isOpen, continuousSMul_inf, continuousSMul_sInf, continuousVAdd_iInf, continuousVAdd_inf, continuousVAdd_sInf, instContinuousSMulForall, instContinuousSMulULift, instContinuousVAddForall, instContinuousVAddULift, smul_set_closure_subset, stabilizer_isOpen, vadd_set_closure_subset	59
Total	62

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd_compHom 📖	mathematical	Continuous DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	ContinuousVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction compHom	—	Continuous.vadd Continuous.comp continuous_fst continuous_snd

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd 📖	mathematical	—	ContinuousVAdd AddOpposite instVAdd instTopologicalSpaceAddOpposite	—	Continuous.comp continuous_op ContinuousVAdd.continuous_vadd Continuous.prodMap continuous_id continuous_unop

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd 📖	mathematical	—	ContinuousVAdd AddSubgroup SetLike.instMembership instSetLike AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup AddAction.toAddSemigroupAction AddAction.instAddAction instTopologicalSpaceSubtype	—	AddSubmonoid.continuousVAdd

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd 📖	mathematical	—	ContinuousVAdd AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction instTopologicalSpaceSubtype	—	Topology.IsInducing.continuousVAdd Topology.IsInducing.id continuous_subtype_val

AddTorsor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedSpace 📖	mathematical	—	ConnectedSpace	—	nonempty Set.image_univ Equiv.range_eq_univ IsPreconnected.image PreconnectedSpace.isPreconnected_univ Continuous.continuousOn Continuous.vadd continuous_id continuous_const

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd 📖	mathematical	—	ContinuousVAdd AddUnits instVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction instTopologicalSpaceAddUnits	—	Topology.IsInducing.continuousVAdd Topology.IsInducing.id continuous_val

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	Continuous	—	—	comp ContinuousSMul.continuous_smul prodMk
vadd 📖	mathematical	Continuous	HVAdd.hVAdd instHVAdd	—	comp ContinuousVAdd.continuous_vadd prodMk

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	ContinuousAt	—	—	Filter.Tendsto.smul
vadd 📖	mathematical	ContinuousAt	HVAdd.hVAdd instHVAdd	—	Filter.Tendsto.vadd

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	ContinuousOn	—	—	ContinuousWithinAt.smul
vadd 📖	mathematical	ContinuousOn	HVAdd.hVAdd instHVAdd	—	ContinuousWithinAt.vadd

ContinuousSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousConstSMul 📖	mathematical	—	ContinuousConstSMul	—	Continuous.comp continuous_smul Continuous.prodMk continuous_const continuous_id
continuous_smul 📖	mathematical	—	Continuous instTopologicalSpaceProd	—	—
induced 📖	mathematical	—	ContinuousSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TopologicalSpace.induced DFunLike.coe	—	continuous_induced_rng map_smul SemilinearMapClass.toMulActionSemiHomClass Continuous.comp' continuous_smul Continuous.prodMk Continuous.fst continuous_id' continuous_induced_dom Continuous.snd
op 📖	mathematical	—	ContinuousSMul MulOpposite MulOpposite.instTopologicalSpaceMulOpposite	—	IsCentralScalar.op_smul_eq_smul continuous_smul Continuous.comp Continuous.prodMap MulOpposite.continuous_unop continuous_id

ContinuousVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousConstVAdd 📖	mathematical	—	ContinuousConstVAdd	—	Continuous.comp continuous_vadd Continuous.prodMk continuous_const continuous_id
continuous_vadd 📖	mathematical	—	Continuous instTopologicalSpaceProd HVAdd.hVAdd instHVAdd	—	—
op 📖	mathematical	—	ContinuousVAdd AddOpposite AddOpposite.instTopologicalSpaceAddOpposite	—	IsCentralVAdd.op_vadd_eq_vadd continuous_vadd Continuous.comp Continuous.prodMap AddOpposite.continuous_unop continuous_id

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	ContinuousWithinAt	—	—	Filter.Tendsto.smul
vadd 📖	mathematical	ContinuousWithinAt	HVAdd.hVAdd instHVAdd	—	Filter.Tendsto.vadd

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
top_smul_nhds_zero 📖	mathematical	—	Filter instSMul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero MulActionWithZero.toSMulWithZero Top.top instTop nhds	—	HasBasis.eq_top_iff HasBasis.smul hasBasis_top basis_sets Set.univ_smul_nhds_zero

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	Filter.Tendsto nhds	—	—	comp Continuous.tendsto ContinuousSMul.continuous_smul prodMk_nhds
smul_const 📖	—	Filter.Tendsto nhds	—	—	smul tendsto_const_nhds
vadd 📖	mathematical	Filter.Tendsto nhds	HVAdd.hVAdd instHVAdd	—	comp Continuous.tendsto ContinuousVAdd.continuous_vadd prodMk_nhds
vadd_const 📖	mathematical	Filter.Tendsto nhds	HVAdd.hVAdd instHVAdd	—	vadd tendsto_const_nhds

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	Inseparable	—	—	map prod ContinuousSMul.continuous_smul
vadd 📖	mathematical	Inseparable	HVAdd.hVAdd instHVAdd	—	map prod ContinuousVAdd.continuous_vadd

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_set 📖	mathematical	IsCompact	Set Set.smul	—	Set.image_smul_prod image prod ContinuousSMul.continuous_smul
vadd_set 📖	mathematical	IsCompact	HVAdd.hVAdd Set instHVAdd Set.vadd	—	Set.vadd_image_prod image prod ContinuousVAdd.continuous_vadd

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul	—	Continuous.comp' ContinuousSMul.continuous_smul Continuous.prodMk Continuous.fst continuous_id' continuous_const Continuous.snd smul_assoc one_smul

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul_compHom 📖	mathematical	Continuous DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	ContinuousSMul SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction compHom	—	Continuous.smul Continuous.comp continuous_fst continuous_snd

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul MulOpposite instSMul instTopologicalSpaceMulOpposite	—	Continuous.comp continuous_op ContinuousSMul.continuous_smul Continuous.prodMap continuous_id continuous_unop

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul instSMul instTopologicalSpaceProd	—	Continuous.prodMk Continuous.smul continuous_fst Continuous.comp continuous_snd
continuousVAdd 📖	mathematical	—	ContinuousVAdd instVAdd instTopologicalSpaceProd	—	Continuous.prodMk Continuous.vadd continuous_fst Continuous.comp continuous_snd

SMulMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul SetLike.instMembership SetLike.smul instTopologicalSpaceSubtype	—	Topology.IsInducing.continuousSMul Topology.IsInducing.subtypeVal continuous_id

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
univ_smul_nhds_zero 📖	mathematical	Set Filter Filter.instMembership nhds	smul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero MulActionWithZero.toSMulWithZero univ	—	eq_univ_of_forall Filter.Tendsto.smul Filter.tendsto_id tendsto_const_nhds zero_smul Filter.nonempty_of_mem inter_mem_nhdsWithin Filter.mem_map inv_smul_smul₀

Specializes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	—	Specializes	—	—	map prod ContinuousSMul.continuous_smul
vadd 📖	mathematical	Specializes	HVAdd.hVAdd instHVAdd	—	map prod ContinuousVAdd.continuous_vadd

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction MulAction.instMulAction instTopologicalSpaceSubtype	—	Submonoid.continuousSMul

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike smul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instTopologicalSpaceSubtype	—	Topology.IsInducing.continuousSMul Topology.IsInducing.id continuous_subtype_val

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	Topology.IsInducing Continuous	ContinuousSMul	—	continuous_iff Continuous.smul Continuous.comp continuous_fst continuous continuous_snd
continuousVAdd 📖	mathematical	Topology.IsInducing Continuous HVAdd.hVAdd instHVAdd	ContinuousVAdd	—	continuous_iff Continuous.vadd Continuous.comp continuous_fst continuous continuous_snd

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul Units instSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instTopologicalSpaceUnits	—	Topology.IsInducing.continuousSMul Topology.IsInducing.id continuous_val

VAddMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousVAdd 📖	mathematical	—	ContinuousVAdd SetLike.instMembership SetLike.vadd instTopologicalSpaceSubtype	—	Topology.IsInducing.continuousVAdd Topology.IsInducing.subtypeVal continuous_id

(root)

Definitions

Name	Category	Theorems
ContinuousSMul 📖	CompData	80 math math: continuousSMul_sphere_ball, IsModuleTopology.toContinuousSMul, continuousSMul_sphere_sphere, ContinuousLinearMap.continuousSMul, continuousSMul_of_algebraMap, AddGroup.continuousSMul_int, SchwartzMap.instContinuousSMul, WithSeminorms.continuousSMul, TopModuleCat.continuousSMul, UniformOnFun.continuousSMul_induced_of_image_bounded, ContinuousAlternatingMap.instContinuousSMul, Topology.IsInducing.continuousSMul, DiscreteTopology.instContinuousSMul, MvPowerSeries.WithPiTopology.instContinuousSMul, IntermediateField.continuousSMul, CStarMatrix.instContinuousSMul, AddMonoid.continuousSMul_nat, ProperSMul.toContinuousSMul, ModuleTopology.continuousSMul, UniformConvergenceCLM.continuousSMul, IsBoundedSMul.continuousSMul, continuousSMul_closedBall_ball, IntermediateField.botContinuousSMul, continuousSMul_sphere_closedBall, UniformFun.continuousSMul_induced_of_range_bounded, MeasureTheory.FiniteMeasure.instContinuousSMulNNReal, NNRat.instContinuousSMulOfIsScalarTowerOfRat, Circle.instContinuousSMul, WeakBilin.instContinuousSMul, CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber, Subfield.continuousSMul, ContinuousSMul.op, properSMul_iff_continuousSMul_ultrafilter_tendsto_t2, ContinuousLinearMapWOT.instContinuousSMul, instContinuousSMulULift, UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp, continuousSMul_induced, ContinuousMap.instContinuousSMul, continuousSMul_inf, Subgroup.continuousSMul, QuotientGroup.instContinuousSMul, WithCStarModule.instContinuousSMul, Prod.continuousSMul, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul, NNReal.instContinuousSMulOfReal, Subring.continuousSMul, SMulMemClass.continuousSMul, TrivSqZeroExt.instContinuousSMul, instContinuousSMulSubtypeLeOfNat, WeakDual.instContinuousSMul, Submonoid.continuousSMul, WeakSpace.instContinuousSMul, ContinuousMultilinearMap.instContinuousSMul, MulOpposite.continuousSMul, NNRat.instContinuousSMulNNReal, continuousSMul_inducedₛₗ, ContDiffMapSupportedIn.continuousSMul, continuousSMul_iff_stabilizer_isOpen, continuousSMul_closedBall_closedBall, properSMul_iff_continuousSMul_ultrafilter_tendsto, ContinuousSMul.of_basis_zero, MulAction.continuousSMul_compHom, Submodule.continuousSMul_quotient, CompactConvergenceCLM.continuousSMul, IsScalarTower.continuousSMul, Subalgebra.continuousSMul, TestFunction.instContinuousSMulReal, Subsemiring.continuousSMul, UniformOnFun.continuousSMul_submodule_of_image_bounded, Units.continuousSMul, ContinuousMul.to_continuousSMul, SeparationQuotient.instContinuousSMul, instContinuousSMulMatrix, CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjCarrier, NNRat.instContinuousSMulRatReal, ModuleFilterBasis.continuousSMul, MeasureTheory.Lp.instContinuousSMulDomMulAct, ContinuousMul.to_continuousSMul_op, ContinuousSMul.induced, ContinuousSMul.of_nhds_zero
ContinuousVAdd 📖	CompData	19 math math: AddSubmonoid.continuousVAdd, ContinuousMap.instContinuousVAdd, Topology.IsInducing.continuousVAdd, AddAction.continuousVAdd_compHom, QuotientAddGroup.instContinuousVAdd, AddOpposite.continuousVAdd, instContinuousVAddULift, VAddMemClass.continuousVAdd, IsTopologicalAddTorsor.toContinuousVAdd, AddSubgroup.continuousVAdd, ProperVAdd.toContinuousVAdd, MeasureTheory.Lp.instContinuousVAddDomAddAct, AddUnits.continuousVAdd, properVAdd_iff_continuousVAdd_ultrafilter_tendsto, ContinuousAdd.to_continuousVAdd_op, ContinuousVAdd.op, continuousVAdd_inf, Prod.continuousVAdd, ContinuousAdd.to_continuousVAdd
MulAction 📖	CompData	2 math math: SubMulAction.ofFixingSubgroup_of_eq_apply, SubMulAction.ofFixingSubgroup_of_eq_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul_iInf 📖	mathematical	ContinuousSMul	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuousSMul_sInf Set.forall_mem_range
continuousSMul_iff_stabilizer_isOpen 📖	mathematical	—	ContinuousSMul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction IsOpen SetLike.coe Subgroup Subgroup.instSetLike MulAction.stabilizer	—	stabilizer_isOpen continuous_prod_of_discrete_right continuous_discrete_rng Set.nonempty_iff_empty_ne Set.ext eq_inv_smul_iff IsOpen.preimage Continuous.fun_mul IsTopologicalGroup.toContinuousMul continuous_id' continuous_const
continuousSMul_inf 📖	mathematical	—	ContinuousSMul TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	inf_eq_iInf continuousSMul_iInf
continuousSMul_sInf 📖	mathematical	ContinuousSMul	InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sInf_singleton continuous_sInf_rng continuous_sInf_dom₂ ContinuousSMul.continuous_smul
continuousVAdd_iInf 📖	mathematical	ContinuousVAdd	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuousVAdd_sInf Set.forall_mem_range
continuousVAdd_inf 📖	mathematical	—	ContinuousVAdd TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	inf_eq_iInf continuousVAdd_iInf
continuousVAdd_sInf 📖	mathematical	ContinuousVAdd	InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sInf_singleton continuous_sInf_rng continuous_sInf_dom₂ ContinuousVAdd.continuous_vadd
instContinuousSMulForall 📖	mathematical	ContinuousSMul	Pi.instSMul Pi.topologicalSpace	—	continuous_pi Continuous.comp Continuous.smul continuous_fst continuous_snd Continuous.prodMk continuous_apply
instContinuousSMulULift 📖	mathematical	—	ContinuousSMul ULift.smulLeft ULift.topologicalSpace	—	Continuous.comp₂ ContinuousSMul.continuous_smul Continuous.comp continuous_uliftDown continuous_fst continuous_snd
instContinuousVAddForall 📖	mathematical	ContinuousVAdd	Pi.instVAdd Pi.topologicalSpace	—	continuous_pi Continuous.comp Continuous.vadd continuous_fst continuous_snd Continuous.prodMk continuous_apply
instContinuousVAddULift 📖	mathematical	—	ContinuousVAdd ULift.vaddLeft ULift.topologicalSpace	—	Continuous.comp₂ ContinuousVAdd.continuous_vadd Continuous.comp continuous_uliftDown continuous_fst continuous_snd
smul_set_closure_subset 📖	mathematical	—	Set Set.instHasSubset Set.smul closure	—	Set.smul_subset_iff map_mem_closure₂ ContinuousSMul.continuous_smul Set.smul_mem_smul
stabilizer_isOpen 📖	mathematical	—	IsOpen SetLike.coe Subgroup Subgroup.instSetLike MulAction.stabilizer	—	IsOpen.preimage Continuous.smul continuous_id' continuous_const isOpen_discrete
vadd_set_closure_subset 📖	mathematical	—	Set Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vadd closure	—	Set.vadd_subset_iff map_mem_closure₂ ContinuousVAdd.continuous_vadd Set.vadd_mem_vadd

---

← Back to Index