ConstMulAction

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

Statistics

Metric	Count
Definitions `ContinuousConstSMul`, `ContinuousConstVAdd`, `smul`, `smulOfNeZero`, `vadd`, `ProperlyDiscontinuousSMul`, `ProperlyDiscontinuousVAdd`	7
Theorems `discreteTopology_iff`, `t1Space_iff`, `isOpenQuotientMap_quotientMk`, `continuousConstVAdd`, `continuousConstVAdd`, `const_smul`, `const_vadd`, `const_smul`, `const_vadd`, `continuous_const_smul`, `op`, `secondCountableTopology`, `continuous_const_vadd`, `op`, `secondCountableTopology`, `const_smul`, `const_vadd`, `const_smul`, `const_vadd`, `smul`, `vadd`, `const_smul`, `const_vadd`, `to_properlyDiscontinuousSMul`, `to_properlyDiscontinuousVAdd`, `comp_smul`, `comp_smul`, `smulOfNeZero_apply`, `smulOfNeZero_symm_apply`, `smul_apply`, `smul_symm_apply`, `vadd_apply`, `vadd_symm_apply`, `const_smul`, `const_vadd`, `smul`, `smul_of_ne_zero`, `smul₀`, `vadd`, `smul`, `vadd`, `smul`, `smul_left`, `smul₀`, `vadd`, `vadd_left`, `continuousAt_const_smul_iff`, `continuousOn_const_smul_iff`, `continuousWithinAt_const_smul_iff`, `continuous_const_smul_iff`, `isClosedMap_smul`, `isHomeomorph_smul`, `isOpenMap_smul`, `isQuotientMap_nsmul`, `isQuotientMap_smul`, `isQuotientMap_zsmul`, `smul_mem_nhds_smul_iff`, `tendsto_const_smul_iff`, `discreteTopology_iff`, `t1Space_iff`, `isOpenQuotientMap_quotientMk`, `continuousConstSMul`, `continuousConstSMul'`, `continuousConstVAdd'`, `continuousConstSMul`, `continuousConstVAdd`, `exists_nhds_disjoint_image`, `exists_nhds_image_smul_eq_self`, `finite_disjoint_inter_image`, `finite_stabilizer`, `finite_stabilizer'`, `exists_nhds_disjoint_image`, `exists_nhds_image_vadd_eq_self`, `finite_disjoint_inter_image`, `finite_stabilizer`, `finite_stabilizer'`, `const_smul`, `const_vadd`, `continuousConstSMul`, `continuousConstVAdd`, `continuousConstSMul`, `closure_smul`, `closure_smul₀`, `closure_smul₀'`, `closure_vadd`, `continuousAt_const_smul_iff`, `continuousAt_const_smul_iff₀`, `continuousAt_const_vadd_iff`, `continuousOn_const_smul_iff`, `continuousOn_const_smul_iff₀`, `continuousOn_const_vadd_iff`, `continuousWithinAt_const_smul_iff`, `continuousWithinAt_const_smul_iff₀`, `continuousWithinAt_const_vadd_iff`, `continuous_const_smul_iff`, `continuous_const_smul_iff₀`, `continuous_const_vadd_iff`, `instContinuousConstSMulForall`, `instContinuousConstSMulOrderDual`, `instContinuousConstSMulULift`, `instContinuousConstVAddForall`, `instContinuousConstVAddOrderDual`, `instContinuousConstVAddULift`, `interior_smul`, `interior_smul₀`, `interior_vadd`, `isClosedMap_smul`, `isClosedMap_smul_of_ne_zero`, `isClosedMap_smul₀`, `isClosedMap_vadd`, `isClosed_setOf_map_smul`, `isHomeomorph_smul`, `isHomeomorph_smul₀`, `isHomeomorph_vadd`, `isOpenMap_quotient_mk'_add`, `isOpenMap_quotient_mk'_mul`, `isOpenMap_smul`, `isOpenMap_smul₀`, `isOpenMap_vadd`, `nhds_smul`, `nhds_smul₀`, `nhds_vadd`, `punctured_nhds_smul`, `punctured_nhds_smul₀`, `punctured_nhds_vadd`, `set_smul_closure_subset`, `set_smul_mem_nhds_zero_iff`, `set_vadd_closure_subset`, `smul_closure_orbit_subset`, `smul_closure_subset`, `smul_mem_nhds_self`, `smul_mem_nhds_smul`, `smul_mem_nhds_smul_iff`, `smul_mem_nhds_smul_iff₀`, `smul_mem_nhds_smul₀`, `subset_interior_smul_right`, `subset_interior_vadd_right`, `t2Space_of_properlyDiscontinuousSMul_of_t2Space`, `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`, `tendsto_const_smul_iff`, `tendsto_const_smul_iff₀`, `tendsto_const_vadd_iff`, `vadd_closure_orbit_subset`, `vadd_closure_subset`, `vadd_mem_nhds_self`, `vadd_mem_nhds_vadd`, `vadd_mem_nhds_vadd_iff`	147
Total	154

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenQuotientMap_quotientMk` 📖	mathematical	—	`IsOpenQuotientMap` `orbitRel` `instTopologicalSpaceQuotient`	—	`Quot.mk_surjective` `isOpenMap_quotient_mk'_add`

AddAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteTopology_iff` 📖	mathematical	—	`DiscreteTopology` `IsOpen` `Set` `Set.instSingletonSet`	—	`discreteTopology_iff_isOpen_singleton` `AddAction.exists_vadd_eq` `Set.image_singleton` `Set.image_vadd` `IsOpen.vadd`
`t1Space_iff` 📖	mathematical	—	`T1Space` `IsClosed` `Set` `Set.instSingletonSet`	—	`isClosed_singleton` `AddAction.exists_vadd_eq` `Set.image_singleton` `Set.image_vadd` `IsClosed.vadd`

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `AddOpposite` `instTopologicalSpaceAddOpposite` `instVAdd`	—	`Continuous.comp` `continuous_op` `Continuous.const_vadd` `continuous_unop`

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `AddUnits` `instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`ContinuousConstVAdd.continuous_const_vadd`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`Continuous`	—	—	`comp` `ContinuousConstSMul.continuous_const_smul`
`const_vadd` 📖	mathematical	`Continuous`	`HVAdd.hVAdd` `instHVAdd`	—	`comp` `ContinuousConstVAdd.continuous_const_vadd`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`ContinuousAt`	—	—	`Filter.Tendsto.const_smul`
`const_vadd` 📖	mathematical	`ContinuousAt`	`HVAdd.hVAdd` `instHVAdd`	—	`Filter.Tendsto.const_vadd`

ContinuousConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_const_smul` 📖	mathematical	—	`Continuous`	—	—
`op` 📖	mathematical	—	`ContinuousConstSMul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul` `continuous_const_smul`
`secondCountableTopology` 📖	mathematical	—	`SecondCountableTopology` `MulAction.orbitRel` `instTopologicalSpaceQuotient`	—	`TopologicalSpace.Quotient.secondCountableTopology` `isOpenMap_quotient_mk'_mul`

ContinuousConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_const_vadd` 📖	mathematical	—	`Continuous` `HVAdd.hVAdd` `instHVAdd`	—	—
`op` 📖	mathematical	—	`ContinuousConstVAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd` `continuous_const_vadd`
`secondCountableTopology` 📖	mathematical	—	`SecondCountableTopology` `AddAction.orbitRel` `instTopologicalSpaceQuotient`	—	`TopologicalSpace.Quotient.secondCountableTopology` `isOpenMap_quotient_mk'_add`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`ContinuousOn`	—	—	`ContinuousWithinAt.const_smul`
`const_vadd` 📖	mathematical	`ContinuousOn`	`HVAdd.hVAdd` `instHVAdd`	—	`ContinuousWithinAt.const_vadd`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`ContinuousWithinAt`	—	—	`Filter.Tendsto.const_smul`
`const_vadd` 📖	mathematical	`ContinuousWithinAt`	`HVAdd.hVAdd` `instHVAdd`	—	`Filter.Tendsto.const_vadd`

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`Dense`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`dense_iff_closure_eq` `closure_smul` `Set.smul_set_univ`
`vadd` 📖	mathematical	`Dense`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`dense_iff_closure_eq` `closure_vadd` `Set.vadd_set_univ`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`Filter.Tendsto` `nhds`	—	—	`comp` `Continuous.tendsto` `ContinuousConstSMul.continuous_const_smul`
`const_vadd` 📖	mathematical	`Filter.Tendsto` `nhds`	`HVAdd.hVAdd` `instHVAdd`	—	`comp` `Continuous.tendsto` `ContinuousConstVAdd.continuous_const_vadd`

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_properlyDiscontinuousSMul` 📖	mathematical	—	`ProperlyDiscontinuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.toFinite` `Subtype.finite`
`to_properlyDiscontinuousVAdd` 📖	mathematical	—	`ProperlyDiscontinuousVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.toFinite` `Subtype.finite`

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_smul` 📖	mathematical	`HasCompactMulSupport`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`comp_homeomorph`

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_smul` 📖	mathematical	`HasCompactSupport`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`comp_homeomorph`

Homeomorph

Definitions

Name	Category	Theorems
`smul` 📖	CompOp	2 math math: `smul_symm_apply`, `smul_apply`
`smulOfNeZero` 📖	CompOp	2 math math: `smulOfNeZero_symm_apply`, `smulOfNeZero_apply`
`vadd` 📖	CompOp	2 math math: `vadd_symm_apply`, `vadd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulOfNeZero_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `smulOfNeZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	—
`smulOfNeZero_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `smulOfNeZero` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`smul_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `vadd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`vadd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm` `vadd` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`Inseparable`	—	—	`map` `ContinuousConstSMul.continuous_const_smul`
`const_vadd` 📖	mathematical	`Inseparable`	`HVAdd.hVAdd` `instHVAdd`	—	`map` `ContinuousConstVAdd.continuous_const_vadd`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	—	`IsClosed` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isClosedMap_smul`
`smul_of_ne_zero` 📖	mathematical	—	`IsClosed` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`isClosedMap_smul_of_ne_zero`
`smul₀` 📖	mathematical	—	`IsClosed` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `MulActionWithZero.toSMulWithZero`	—	`isClosedMap_smul₀`
`vadd` 📖	mathematical	—	`IsClosed` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`isClosedMap_vadd`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`IsCompact`	`Set` `Set.smulSet`	—	`image` `Continuous.const_smul` `continuous_id`
`vadd` 📖	mathematical	`IsCompact`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet`	—	`image` `Continuous.const_vadd` `continuous_id`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`IsOpen`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isOpenMap_smul`
`smul_left` 📖	mathematical	`IsOpen`	`Set` `Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.iUnion_smul_set` `isOpen_biUnion` `smul`
`smul₀` 📖	mathematical	`IsOpen`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`isOpenMap_smul₀`
`vadd` 📖	mathematical	`IsOpen`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`isOpenMap_vadd`
`vadd_left` 📖	mathematical	`IsOpen`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.iUnion_vadd_set` `isOpen_biUnion` `vadd`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_const_smul_iff` 📖	mathematical	`IsUnit`	`ContinuousAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`continuousAt_const_smul_iff` `Units.continuousConstSMul`
`continuousOn_const_smul_iff` 📖	mathematical	`IsUnit`	`ContinuousOn` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`continuousOn_const_smul_iff` `Units.continuousConstSMul`
`continuousWithinAt_const_smul_iff` 📖	mathematical	`IsUnit`	`ContinuousWithinAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`continuousWithinAt_const_smul_iff` `Units.continuousConstSMul`
`continuous_const_smul_iff` 📖	mathematical	`IsUnit`	`Continuous` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`continuous_const_smul_iff` `Units.continuousConstSMul`
`isClosedMap_smul` 📖	mathematical	`IsUnit`	`IsClosedMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`isClosedMap_smul` `Units.continuousConstSMul`
`isHomeomorph_smul` 📖	mathematical	`IsUnit`	`IsHomeomorph` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`isHomeomorph_smul` `Units.continuousConstSMul`
`isOpenMap_smul` 📖	mathematical	`IsUnit`	`IsOpenMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`isOpenMap_smul` `Units.continuousConstSMul`
`isQuotientMap_nsmul` 📖	mathematical	`Topology.IsQuotientMap` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`AddMonoid.toNatSMul`	—	`isQuotientMap_smul` `AddCommMonoid.nat_isScalarTower` `map_nsmul` `AddMonoidHom.instAddMonoidHomClass` `nsmul_one`
`isQuotientMap_smul` 📖	—	`Topology.IsQuotientMap` `DFunLike.coe` `MulActionHom` `instFunLikeMulActionHom` `IsUnit` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`Topology.IsQuotientMap.of_comp_isQuotientMap` `smul_assoc` `one_smul` `map_smul` `instMulActionSemiHomClassMulActionHom` `Topology.IsQuotientMap.comp` `IsHomeomorph.isQuotientMap` `isHomeomorph_smul`
`isQuotientMap_zsmul` 📖	mathematical	`Topology.IsQuotientMap` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	`SubNegMonoid.toZSMul`	—	`isQuotientMap_smul` `AddCommGroup.intIsScalarTower` `map_zsmul` `AddMonoidHom.instAddMonoidHomClass` `zsmul_one`
`smul_mem_nhds_smul_iff` 📖	mathematical	`IsUnit`	`Set` `Filter` `Filter.instMembership` `nhds` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Set.smulSet`	—	`smul_mem_nhds_smul_iff` `Units.continuousConstSMul`
`tendsto_const_smul_iff` 📖	mathematical	`IsUnit`	`Filter.Tendsto` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `nhds`	—	`tendsto_const_smul_iff` `Units.continuousConstSMul`

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenQuotientMap_quotientMk` 📖	mathematical	—	`IsOpenQuotientMap` `orbitRel` `instTopologicalSpaceQuotient`	—	`Quot.mk_surjective` `isOpenMap_quotient_mk'_mul`

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discreteTopology_iff` 📖	mathematical	—	`DiscreteTopology` `IsOpen` `Set` `Set.instSingletonSet`	—	`discreteTopology_iff_isOpen_singleton` `MulAction.exists_smul_eq` `Set.image_singleton` `Set.image_smul` `IsOpen.smul`
`t1Space_iff` 📖	mathematical	—	`T1Space` `IsClosed` `Set` `Set.instSingletonSet`	—	`isClosed_singleton` `MulAction.exists_smul_eq` `Set.image_singleton` `Set.image_smul` `IsClosed.smul`

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `MulOpposite` `instTopologicalSpaceMulOpposite` `instSMul`	—	`Continuous.comp` `continuous_op` `Continuous.const_smul` `continuous_unop`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstSMul'` 📖	mathematical	—	`ContinuousConstSMul` `OrderDual` `instSMul'`	—	—
`continuousConstVAdd'` 📖	mathematical	—	`ContinuousConstVAdd` `OrderDual` `instVAdd'`	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `instTopologicalSpaceProd` `instSMul`	—	`Continuous.prodMk` `Continuous.const_smul` `continuous_fst` `continuous_snd`
`continuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `instTopologicalSpaceProd` `instVAdd`	—	`Continuous.prodMk` `Continuous.const_vadd` `continuous_fst` `continuous_snd`

ProperlyDiscontinuousSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nhds_disjoint_image` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.image`	—	`not_imp_not` `exists_nhds_image_smul_eq_self`
`exists_nhds_image_smul_eq_self` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Set.Finite.subset` `finite_disjoint_inter_image` `Filter.inter_mem` `Filter.iInter_mem` `Continuous.continuousAt` `ContinuousConstSMul.continuous_const_smul` `Set.mem_iInter` `Set.mem_inter_iff` `Disjoint.le_bot` `t2_separation_nhds`
`finite_disjoint_inter_image` 📖	mathematical	`IsCompact`	`Set.Finite` `setOf` `Set.Nonempty` `Set` `Set.instInter` `Set.image`	—	—
`finite_stabilizer` 📖	mathematical	—	`Set.Finite` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulAction.stabilizer`	—	`finite_stabilizer'`
`finite_stabilizer'` 📖	mathematical	—	`Set.Finite` `setOf`	—	`finite_disjoint_inter_image` `isCompact_singleton`

ProperlyDiscontinuousVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nhds_disjoint_image` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.image` `HVAdd.hVAdd` `instHVAdd`	—	`not_imp_not` `Set.not_disjoint_iff_nonempty_inter` `exists_nhds_image_vadd_eq_self`
`exists_nhds_image_vadd_eq_self` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `HVAdd.hVAdd` `instHVAdd`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `Set.Finite.subset` `finite_disjoint_inter_image` `Filter.inter_mem` `Filter.iInter_mem` `Continuous.continuousAt` `ContinuousConstVAdd.continuous_const_vadd` `Set.mem_iInter` `Set.mem_inter_iff` `Disjoint.le_bot` `t2_separation_nhds`
`finite_disjoint_inter_image` 📖	mathematical	`IsCompact`	`Set.Finite` `setOf` `Set.Nonempty` `Set` `Set.instInter` `Set.image` `HVAdd.hVAdd` `instHVAdd`	—	—
`finite_stabilizer` 📖	mathematical	—	`Set.Finite` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddAction.stabilizer`	—	`finite_stabilizer'`
`finite_stabilizer'` 📖	mathematical	—	`Set.Finite` `setOf` `HVAdd.hVAdd` `instHVAdd`	—	`Set.mem_singleton_iff` `Set.singleton_inter_nonempty` `Set.image_singleton` `finite_disjoint_inter_image` `isCompact_singleton`

Specializes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul` 📖	—	`Specializes`	—	—	`map` `ContinuousConstSMul.continuous_const_smul`
`const_vadd` 📖	mathematical	`Specializes`	`HVAdd.hVAdd` `instHVAdd`	—	`map` `ContinuousConstVAdd.continuous_const_vadd`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstSMul` 📖	mathematical	`Topology.IsInducing`	`ContinuousConstSMul`	—	`continuous_iff` `Continuous.const_smul` `continuous`
`continuousConstVAdd` 📖	mathematical	`Topology.IsInducing` `HVAdd.hVAdd` `instHVAdd`	`ContinuousConstVAdd`	—	`continuous_iff` `Continuous.const_vadd` `continuous`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `Units` `instSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`ContinuousConstSMul.continuous_const_smul`

(root)

Definitions

Name	Category	Theorems
`ContinuousConstSMul` 📖	CompData	33 math math: `MulOpposite.continuousConstSMul`, `OrderDual.continuousConstSMul'`, `isQuotientCoveringMap_iff`, `Topology.IsInducing.continuousConstSMul`, `UniformContinuousConstSMul.to_continuousConstSMul`, `ContinuousAlternatingMap.instContinuousConstSMul`, `WeakDual.instContinuousConstSMul`, `IsIsometricSMul.to_continuousConstSMul`, `AddMonoid.continuousConstSMul_nat`, `isQuotientCoveringMap_iff_isCoveringMap_and`, `instContinuousConstSMulMatrix`, `Prod.continuousConstSMul`, `ContinuousMultilinearMap.instContinuousConstSMul`, `DivisionRing.continuousConstSMul_rat`, `IsQuotientCoveringMap.toContinuousConstSMul`, `AddGroup.continuousConstSMul_int`, `ConjAct.units_continuousConstSMul`, `Units.continuousConstSMul`, `ContinuousLinearMap.continuousConstSMul`, `IsScalarTower.continuousConstSMul`, `SeparationQuotient.instContinuousConstSMul`, `ContinuousSMul.continuousConstSMul`, `instContinuousConstSMulULift`, `SMulCommClass.continuousConstSMul`, `UniformConvergenceCLM.instContinuousConstSMul`, `QuotientGroup.instContinuousConstSMul`, `UpperHalfPlane.instContinuousGLSMul`, `ContinuousMap.instContinuousConstSMul`, `ContinuousLinearMap.continuousConstSMul_apply`, `instContinuousConstSMulSubtypeLeOfNat`, `instContinuousConstSMulOrderDual`, `ContinuousConstSMul.op`, `TrivSqZeroExt.instContinuousConstSMul`
`ContinuousConstVAdd` 📖	CompData	19 math math: `isAddQuotientCoveringMap_iff_isCoveringMap_and`, `VAddCommClass.continuousConstVAdd`, `instContinuousConstVAddULift`, `VAddAssocClass.continuousConstVAdd`, `UniformContinuousConstVAdd.to_continuousConstVAdd`, `IsIsometricVAdd.to_continuousConstVAdd`, `ContinuousMap.instContinuousConstVAdd`, `ContinuousConstVAdd.op`, `instContinuousConstVAddOrderDual`, `OrderDual.continuousConstVAdd'`, `QuotientAddGroup.instContinuousConstVAdd`, `Prod.continuousConstVAdd`, `AddUnits.continuousConstVAdd`, `AddOpposite.continuousConstVAdd`, `ContinuousVAdd.continuousConstVAdd`, `isAddQuotientCoveringMap_iff`, `IsAddQuotientCoveringMap.toContinuousConstVAdd`, `SeparationQuotient.instContinuousConstVAdd`, `Topology.IsInducing.continuousConstVAdd`
`ProperlyDiscontinuousSMul` 📖	CompData	4 math math: `Finite.to_properlyDiscontinuousSMul`, `Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite`, `Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite`, `properlyDiscontinuousSMul_iff_properSMul`
`ProperlyDiscontinuousVAdd` 📖	CompData	4 math math: `Finite.to_properlyDiscontinuousVAdd`, `AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite`, `AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_smul` 📖	mathematical	—	`closure` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.image_closure`
`closure_smul₀` 📖	mathematical	—	`closure` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `MulActionWithZero.toSMulWithZero`	—	`eq_or_ne` `Set.eq_empty_or_nonempty` `Set.smul_set_empty` `IsClosed.closure_eq` `Set.zero_smul_set` `Set.Nonempty.closure` `closure_singleton` `closure_smul₀'`
`closure_smul₀'` 📖	mathematical	—	`closure` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Homeomorph.image_closure`
`closure_vadd` 📖	mathematical	—	`closure` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.image_closure`
`continuousAt_const_smul_iff` 📖	mathematical	—	`ContinuousAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`tendsto_const_smul_iff`
`continuousAt_const_smul_iff₀` 📖	mathematical	—	`ContinuousAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`continuousAt_const_smul_iff` `Units.continuousConstSMul`
`continuousAt_const_vadd_iff` 📖	mathematical	—	`ContinuousAt` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`tendsto_const_vadd_iff`
`continuousOn_const_smul_iff` 📖	mathematical	—	`ContinuousOn` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`continuousWithinAt_const_smul_iff`
`continuousOn_const_smul_iff₀` 📖	mathematical	—	`ContinuousOn` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`continuousOn_const_smul_iff` `Units.continuousConstSMul`
`continuousOn_const_vadd_iff` 📖	mathematical	—	`ContinuousOn` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`continuousWithinAt_const_vadd_iff`
`continuousWithinAt_const_smul_iff` 📖	mathematical	—	`ContinuousWithinAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`tendsto_const_smul_iff`
`continuousWithinAt_const_smul_iff₀` 📖	mathematical	—	`ContinuousWithinAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`tendsto_const_smul_iff` `Units.continuousConstSMul`
`continuousWithinAt_const_vadd_iff` 📖	mathematical	—	`ContinuousWithinAt` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`tendsto_const_vadd_iff`
`continuous_const_smul_iff` 📖	mathematical	—	`Continuous` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`continuous_const_smul_iff₀` 📖	mathematical	—	`Continuous` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`continuous_const_smul_iff` `Units.continuousConstSMul`
`continuous_const_vadd_iff` 📖	mathematical	—	`Continuous` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`continuous_iff_continuousAt` `continuousAt_const_vadd_iff`
`instContinuousConstSMulForall` 📖	mathematical	`ContinuousConstSMul`	`Pi.topologicalSpace` `Pi.instSMul`	—	`continuous_pi` `Continuous.const_smul` `continuous_apply`
`instContinuousConstSMulOrderDual` 📖	mathematical	—	`ContinuousConstSMul` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instSMul`	—	—
`instContinuousConstSMulULift` 📖	mathematical	—	`ContinuousConstSMul` `ULift.smulLeft`	—	`ContinuousConstSMul.continuous_const_smul`
`instContinuousConstVAddForall` 📖	mathematical	`ContinuousConstVAdd`	`Pi.topologicalSpace` `Pi.instVAdd`	—	`continuous_pi` `Continuous.const_vadd` `continuous_apply`
`instContinuousConstVAddOrderDual` 📖	mathematical	—	`ContinuousConstVAdd` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instVAdd`	—	—
`instContinuousConstVAddULift` 📖	mathematical	—	`ContinuousConstVAdd` `ULift.vaddLeft`	—	`ContinuousConstVAdd.continuous_const_vadd`
`interior_smul` 📖	mathematical	—	`interior` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.image_interior`
`interior_smul₀` 📖	mathematical	—	`interior` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Homeomorph.image_interior`
`interior_vadd` 📖	mathematical	—	`interior` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.image_interior`
`isClosedMap_smul` 📖	mathematical	—	`IsClosedMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.isClosedMap`
`isClosedMap_smul_of_ne_zero` 📖	mathematical	—	`IsClosedMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Homeomorph.isClosedMap`
`isClosedMap_smul₀` 📖	mathematical	—	`IsClosedMap` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `MulActionWithZero.toSMulWithZero`	—	`eq_or_ne` `zero_smul` `isClosedMap_const` `Homeomorph.isClosedMap`
`isClosedMap_vadd` 📖	mathematical	—	`IsClosedMap` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.isClosedMap`
`isClosed_setOf_map_smul` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `setOf`	—	`Set.setOf_forall` `isClosed_iInter` `isClosed_eq` `continuous_apply` `Continuous.const_smul`
`isHomeomorph_smul` 📖	mathematical	—	`IsHomeomorph` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.isHomeomorph`
`isHomeomorph_smul₀` 📖	mathematical	—	`IsHomeomorph` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Homeomorph.isHomeomorph`
`isHomeomorph_vadd` 📖	mathematical	—	`IsHomeomorph` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.isHomeomorph`
`isOpenMap_quotient_mk'_add` 📖	mathematical	—	`IsOpenMap` `AddAction.orbitRel` `instTopologicalSpaceQuotient`	—	`isOpen_coinduced` `AddAction.quotient_preimage_image_eq_union_add` `isOpen_iUnion` `isOpenMap_vadd`
`isOpenMap_quotient_mk'_mul` 📖	mathematical	—	`IsOpenMap` `MulAction.orbitRel` `instTopologicalSpaceQuotient`	—	`isOpen_coinduced` `MulAction.quotient_preimage_image_eq_union_mul` `isOpen_iUnion` `isOpenMap_smul`
`isOpenMap_smul` 📖	mathematical	—	`IsOpenMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.isOpenMap`
`isOpenMap_smul₀` 📖	mathematical	—	`IsOpenMap` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Homeomorph.isOpenMap`
`isOpenMap_vadd` 📖	mathematical	—	`IsOpenMap` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.isOpenMap`
`nhds_smul` 📖	mathematical	—	`nhds` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Filter` `Filter.instSMulFilter`	—	`Homeomorph.map_nhds_eq`
`nhds_smul₀` 📖	mathematical	—	`nhds` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `Filter` `Filter.instSMulFilter`	—	`nhds_smul` `Units.continuousConstSMul`
`nhds_vadd` 📖	mathematical	—	`nhds` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Filter` `Filter.instVAddFilter`	—	`Homeomorph.map_nhds_eq`
`punctured_nhds_smul` 📖	mathematical	—	`nhdsWithin` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter` `Filter.instSMulFilter`	—	`Homeomorph.map_punctured_nhds_eq`
`punctured_nhds_smul₀` 📖	mathematical	—	`nhdsWithin` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter` `Filter.instSMulFilter`	—	`punctured_nhds_smul` `Units.continuousConstSMul`
`punctured_nhds_vadd` 📖	mathematical	—	`nhdsWithin` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter` `Filter.instVAddFilter`	—	`Homeomorph.map_punctured_nhds_eq`
`set_smul_closure_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smul` `closure`	—	`Set.iUnion₂_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `smul_closure_subset` `closure_mono` `Set.subset_biUnion_of_mem`
`set_smul_mem_nhds_zero_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Set.smulSet` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero`	—	`smul_zero` `smul_mem_nhds_smul_iff₀`
`set_vadd_closure_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vadd` `closure`	—	`Set.iUnion_vadd_set` `Set.iUnion₂_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `vadd_closure_subset` `closure_mono` `Set.subset_biUnion_of_mem`
`smul_closure_orbit_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `closure` `MulAction.orbit`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `smul_closure_subset` `closure_mono` `MulAction.smul_orbit_subset`
`smul_closure_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `closure`	—	`Set.MapsTo.image_subset` `Set.MapsTo.closure` `Set.mapsTo_image` `ContinuousConstSMul.continuous_const_smul`
`smul_mem_nhds_self` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`smul_mem_nhds_smul_iff` `inv_mul_cancel` `inv_smul_smul`
`smul_mem_nhds_smul` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.smulSet`	—	`smul_mem_nhds_smul_iff`
`smul_mem_nhds_smul_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Set.smulSet`	—	`Topology.IsOpenEmbedding.image_mem_nhds` `Homeomorph.isOpenEmbedding`
`smul_mem_nhds_smul_iff₀` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `Set.smulSet`	—	`smul_mem_nhds_smul_iff` `Units.continuousConstSMul`
`smul_mem_nhds_smul₀` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `Set.smulSet`	—	`smul_mem_nhds_smul_iff₀`
`subset_interior_smul_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `interior`	—	`interior_maximal` `Set.smul_subset_smul_left` `interior_subset` `IsOpen.smul_left` `isOpen_interior`
`subset_interior_vadd_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `interior`	—	`interior_maximal` `Set.vadd_subset_vadd_left` `interior_subset` `IsOpen.vadd_left` `isOpen_interior`
`t2Space_of_properlyDiscontinuousSMul_of_t2Space` 📖	mathematical	—	`T2Space` `MulAction.orbitRel` `instTopologicalSpaceQuotient`	—	`t2Space_iff_nhds` `isOpenMap_quotient_mk'_mul` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `ProperlyDiscontinuousSMul.finite_disjoint_inter_image` `IsOpenMap.image_mem_nhds` `Filter.inter_mem` `Filter.biInter_mem` `Continuous.continuousAt` `ContinuousConstSMul.continuous_const_smul` `MulAction.disjoint_image_image_iff` `Disjoint.le_bot` `Set.mem_iInter₂` `Set.eq_empty_iff_forall_notMem` `Set.mem_image_of_mem` `t2_separation_nhds`
`t2Space_of_properlyDiscontinuousVAdd_of_t2Space` 📖	mathematical	—	`T2Space` `AddAction.orbitRel` `instTopologicalSpaceQuotient`	—	`t2Space_iff_nhds` `isOpenMap_quotient_mk'_add` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `ProperlyDiscontinuousVAdd.finite_disjoint_inter_image` `IsOpenMap.image_mem_nhds` `Filter.inter_mem` `Filter.biInter_mem` `Continuous.continuousAt` `ContinuousConstVAdd.continuous_const_vadd` `AddAction.disjoint_image_image_iff` `Disjoint.le_bot` `Set.mem_iInter₂` `Set.eq_empty_iff_forall_notMem` `Set.not_nonempty_iff_eq_empty` `Set.mem_image_of_mem` `t2_separation_nhds`
`tendsto_const_smul_iff` 📖	mathematical	—	`Filter.Tendsto` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `nhds`	—	`inv_smul_smul` `Filter.Tendsto.const_smul`
`tendsto_const_smul_iff₀` 📖	mathematical	—	`Filter.Tendsto` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `nhds`	—	`tendsto_const_smul_iff` `Units.continuousConstSMul`
`tendsto_const_vadd_iff` 📖	mathematical	—	`Filter.Tendsto` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `nhds`	—	`neg_vadd_vadd` `Filter.Tendsto.const_vadd`
`vadd_closure_orbit_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `closure` `AddAction.orbit`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `vadd_closure_subset` `closure_mono` `AddAction.vadd_orbit_subset`
`vadd_closure_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `closure`	—	`Set.MapsTo.image_subset` `Set.MapsTo.closure` `Set.mapsTo_image` `ContinuousConstVAdd.continuous_const_vadd`
`vadd_mem_nhds_self` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`vadd_mem_nhds_vadd_iff` `neg_add_cancel` `neg_vadd_vadd`
`vadd_mem_nhds_vadd` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.vaddSet`	—	`vadd_mem_nhds_vadd_iff`
`vadd_mem_nhds_vadd_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `Set.vaddSet`	—	`Topology.IsOpenEmbedding.image_mem_nhds` `Homeomorph.isOpenEmbedding`

---

← Back to Index