Structures · Topology
LocallyConvexSpace
A LocallyConvexSpace is a topological semimodule over an ordered semiring in which convex
neighborhoods of a point form a neighborhood basis at that point.
- Shape
- 2 explicit arguments · adds convex_basis
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 by80
- LocallyConvexSpace.convex_basis
- geometric_hahn_banach_compact_closed
- ConvexOn.exists_affine_le_of_lt
- LocallyConvexSpace.convex_basis_zero
- TestFunction.limitCLM
- RCLike.geometric_hahn_banach_compact_closed
- RCLike.geometric_hahn_banach_closed_point
- ConvexOn.sSup_affine_eq
- ConvexOn.sSup_of_countable_affine_eq
- TestFunction.mkCLM
- ProperCone.dual_flip_dual
- ConvexOn.univ_sSup_affine_eq
- geometric_hahn_banach_closed_point
- ProperCone.hyperplane_separation_point
- ConvexOn.sSup_of_nat_affine_eq
- nhds_hasBasis_absConvex
- nhds_hasBasis_absConvex_open
- Disjoint.exists_open_convexes
- TestFunction.limitCLM.congr_simp
- Convex.toWeakSpace_closure
- LocallyConvexSpace.induced
- IsCompact.extremePoints_nonempty
- ConvexOn.univ_sSup_of_countable_affine_eq
- geometric_hahn_banach_closed_compact
- RCLike.geometric_hahn_banach_point_closed
- TotallyBounded.convexHull
- Convex.locallyPathConnectedSpace
- bernsteinApproximation_uniform
- RCLike.iInter_halfSpaces_eq'
- LocallyConvexSpace.convex_open_basis_zero
- ConvexOn.univ_sSup_of_nat_affine_eq
- LinearEquiv.image_closure_of_convex
- TestFunction.mkCLM_apply
- TotallyBounded.absConvexHull
- ProperCone.hyperplane_separation
- Convex.eventually_nhdsWithin_segment
- LinearMap.image_closure_of_convex
- geometric_hahn_banach_point_point
- PointedCone.minTensorProduct_eq_max_of_simplicial_generating_left
- ProperCone.dual_dual_flip
- totallyBounded_absConvexHull
- RCLike.geometric_hahn_banach_closed_compact
- ConvexOn.real_sSup_of_nat_affine_eq
- ContinuousLinearMap.instLocallyConvexSpace
- Pi.locallyConvexSpace
- totallyBounded_convexHull
- ConvexOn.real_sSup_of_countable_affine_eq
- LocallyConvexSpace.toLocallyPathConnectedSpace
- Prod.locallyConvexSpace
- toWeakSpace_closedConvexHull_eq
Ancestors0
No ancestors.