interior — Mathlib

English

In a topological vector space, the interior of a convex set is convex.

Русский

Во взвешенном топологическом пространстве внутренность выпуклого множества также выпукла.

LaTeX

$$$$\operatorname{Int}(s)\text{ выпукло, если } s\text{ выпукло.}$$$$

Lean4

/-- In a topological vector space, the interior of a convex set is convex. -/
protected theorem interior [ZeroLEOneClass 𝕜] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (interior s) :=
  convex_iff_openSegment_subset.mpr fun _ hx _ hy =>
    hs.openSegment_closure_interior_subset_interior (interior_subset_closure hx) hy

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