Structures · Topology
SeparatelyContinuousMul
A type class encoding that addition is continuous in each argument. This is weaker than
ContinuousMul.
- Defined in
- Mathlib.Topology.Algebra.Monoid.Defs
- Shape
- One type argument · adds continuous_const_mul, continuous_mul_const
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances7
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- AddOpposite
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by172
- Filter.Tendsto.const_mul
- continuous_const_mul
- continuous_mul_const
- Continuous.const_mul
- Filter.Tendsto.mul_const
- Continuous.div_const
- ContinuousOn.const_mul
- Continuous.mul_const
- Homeomorph.mulLeft
- Homeomorph.mulRight
- CFC.conjSqrt
- Filter.Tendsto.div_const
- Homeomorph.mulRight₀
- Homeomorph.mulLeft₀
- ContinuousAt.const_mul
- Submonoid.topologicalClosure
- ContinuousOn.mul_const
- Subsemigroup.topologicalClosure
- Set.isClosed_centralizer
- ContinuousMap.mulRight
- ContinuousAt.mul_const
- OpenSubgroup.isClosed
- isOpenMap_mul_right
- IsSemitopologicalSemiring.continuousNeg_of_mul
- ContinuousMap.mulLeft
- ContinuousOn.div_const
- Subgroup.isOpen_of_mem_nhds
- HasProd.congr_cofinite₀
- Subgroup.isOpen_mono
- ContinuousAt.div_const
- discreteTopology_iff_isOpen_singleton_one
- isOpenMap_mul_left
- QuotientGroup.discreteTopology
- ContinuousWithinAt.mul_const
- isClosedMap_mul_right
- QuotientGroup.isOpenQuotientMap_mk
- Subgroup.isClosed_of_isOpen
- Subgroup.isOpen_of_isClosed_of_finiteIndex
- IsTopologicalGroup.continuous_conj
- IsOpen.leftCoset
- CFC.conjSqrt_apply
- ContinuousWithinAt.const_mul
- QuotientGroup.discreteTopology_iff
- CFC.conjSqrt_conjSqrt_ringInverse
- QuotientGroup.t1Space_iff
- Submonoid.top_closure_mul_self_subset
- SeparatelyContinuousMul.continuous_mul_const
- CFC.ringInverse_conjSqrt
- SeparatelyContinuousMul.continuous_const_mul
- Subgroup.quotient_finite_of_isOpen
Ancestors0
No ancestors.