Structures · Topology
SeparatelyContinuousAdd
A type class encoding that addition is continuous in each argument. This is weaker than
ContinuousAdd.
- Defined in
- Mathlib.Topology.Algebra.Monoid.Defs
- Shape
- One type argument · adds continuous_const_add, continuous_add_const
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Subtype
- Prod
- OrderDual
- ULift
- AddOpposite
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by116
- Continuous.const_add
- continuous_const_add
- Homeomorph.addLeft
- Homeomorph.addRight
- continuous_add_const
- Filter.Tendsto.const_add
- Continuous.add_const
- Filter.Tendsto.add_const
- ContinuousMap.addRight
- ContinuousOn.const_add
- AddSubmonoid.topologicalClosure
- discreteTopology_iff_isOpen_singleton_zero
- AddSubgroup.isOpen_of_mem_nhds
- AddSubsemigroup.topologicalClosure
- AddSubgroup.isOpen_of_isClosed_of_finiteIndex
- ContinuousOn.add_const
- isOpenMap_add_left
- QuotientAddGroup.isOpenQuotientMap_mk
- AddSubgroup.isOpen_mono
- OpenAddSubgroup.isClosed
- QuotientAddGroup.isOpenMap_coe
- QuotientAddGroup.dense_preimage_mk
- isOpenMap_add_right
- ContinuousMap.addRight.congr_simp
- QuotientAddGroup.nhds_eq
- AddSubgroup.isClosed_of_isOpen
- ContinuousAt.const_add
- QuotientAddGroup.discreteTopology
- AddSubgroup.quotient_finite_of_isOpen
- ContinuousWithinAt.const_add
- QuotientAddGroup.discreteTopology_iff
- isClosedMap_add_right
- ContinuousWithinAt.add_const
- IsTopologicalAddGroup.continuous_addConj
- ContinuousAt.add_const
- ContinuousMap.addLeft
- isClosedMap_add_left
- IsOpen.left_addCoset
- closure_subset_add_left_of_mem_nhds_zero_of_neg
- QuotientAddGroup.t1Space_iff
- vadd_connectedComponent
- closure_subset_add_right_of_mem_nhds_zero_of_neg
- SeparatelyContinuousAdd.continuous_const_add
- AddSubmonoid.topologicalClosure_minimal
- Topology.IsInducing.separatelyContinuousAdd
- AddSubgroup.normalCore_isClosed
- MeasureTheory.Content.is_add_left_invariant_innerContent
- SeparatelyContinuousAdd.continuous_add_const
- Filter.map_add_left_nhdsNE
- AddSubmonoid.top_closure_add_self_subset
Ancestors0
No ancestors.