Structures · Topology
ContinuousStar
Basic hypothesis to talk about a topological space with a continuous star operator.
- Defined in
- Mathlib.Topology.Algebra.Star
- Shape
- One type argument · adds continuous_star
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- Real
- Complex
- NNReal
- Matrix
- Units
- ContinuousLinearMapWOT
- Subtype
- Prod
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by590
- cfc
- cfcₙ
- cfcHom
- cfcₙHom
- cfc_apply
- cfcₙ_apply
- cfcₙ_apply_of_not_predicate
- StarAlgebra.elemental
- cfcₙ_congr
- StarSubalgebra.topologicalClosure
- cfc_comp'
- cfc_id
- cfc_congr
- cfcₙ_id
- NonUnitalStarAlgebra.elemental
- selfAdjoint.expUnitary
- cfc_apply_of_not_predicate
- ContinuousStar.continuous_star
- cfc_id'
- cfc.congr_simp
- cfcₙ_apply_of_not_map_zero
- ContinuousMap.compStarAlgHom'
- starL'
- cfcₙ_eq_cfc
- cfcHom_continuous
- cfc_const
- cfc_cases
- NonUnitalStarSubalgebra.topologicalClosure
- cfc_map_spectrum
- cfcHom_id
- cfcₙHom_continuous
- cfc_apply_of_not_continuousOn
- cfcₙ_id'
- cfcₙ_comp'
- QuasispectrumRestricts.nonUnitalStarAlgHom
- SpectrumRestricts.starAlgHom
- cfcₙHom_id
- cfcₙ_apply_of_not_continuousOn
- cfcₙ_mul
- cfcₙ_cases
- ContinuousMapZero.toContinuousMapHom
- ContinuousOn.star
- starL
- selfAdjoint.expUnitary_coe
- cfcₙ.congr_simp
- cfcL
- cfc_pow
- cfcₙL
- cfc_algebraMap
- cfcHom_map_spectrum
Ancestors0
No ancestors.