Structures · Analysis
SeparatingDual
When E is a topological module over a topological ring R, the class SeparatingDual R E
registers that continuous linear forms on E separate points of E.
- Shape
- 2 explicit arguments · adds exists_ne_zero'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- SeparatingDual.exists_ne_zero
- SeparatingDual.eq_iff_forall_dual_eq
- SeparatingDual.exists_eq_one
- SeparatingDual.eq_zero_of_forall_dual_eq_zero
- SeparatingDual.eq_zero_iff_forall_dual_eq_zero
- ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv
- SeparatingDual.exists_separating_of_ne
- SeparatingDual.completeSpace_of_completeSpace_continuousLinearMap
- SeparatingDual.exists_continuousLinearEquiv_apply_eq
- SeparatingDual.exists_ne_zero'
- SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair
- ContinuousLinearMapWOT.ext_dual_iff
- SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap
- SeparatingDual.completeSpace_continuousLinearMap_iff
- SeparatingDual.completeSpace_continuousMultilinearMap_iff
- ContinuousLinearMapWOT.ext_dual
- SeparatingDual.t1Space
- ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iff
- SeparatingDual.instNontrivialContinuousLinearMapIdOfContinuousSMul
- SeparatingDual.t2Space
- instT2SpaceWeakSpaceOfSeparatingDual
- ContinuousLinearMapWOT.isEmbedding_inducingFn
- ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective
- ContinuousLinearMapWOT.instT3Space
- SeparatingDual.dualMap_surjective_iff
- Algebra.IsCentral.instContinuousLinearMap
Ancestors0
No ancestors.