locallyConvexSpace_iff_exists_convex_subset

English

Locally convexity is equivalent to the existence, for every neighborhood of 0, of a convex neighborhood contained in it.

Русский

Локальная выпуклость эквивалентна существованию для каждого окрестности 0 выпуклого подмножества, вложенного в нее.

LaTeX

$$$LocallyConvexSpace 𝕜 E \iff \forall U \in (\\nhds 0), \exists S \in (\\nhds 0), Convex 𝕜 S \\land S \subseteq U$$$

Lean4

theorem locallyConvexSpace_iff_exists_convex_subset :
    LocallyConvexSpace 𝕜 E ↔ ∀ x : E, ∀ U ∈ 𝓝 x, ∃ S ∈ 𝓝 x, Convex 𝕜 S ∧ S ⊆ U :=
  (locallyConvexSpace_iff 𝕜 E).trans (forall_congr' fun _ => hasBasis_self)

Похожие утверждения