closure_openSegment — Mathlib

English

In a well-behaved topological vector space, the closure of the open segment between x and y equals the closed segment between x and y.

Русский

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

LaTeX

$$$$\overline{\operatorname{openSegment}_{\mathbb{K}}(x,y)} = [x -[\mathbb{K}] y].$$$$

Lean4

@[simp]
theorem closure_openSegment (x y : E) : closure (openSegment 𝕜 x y) = [x -[𝕜] y] :=
  by
  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
  exact
    (image_closure_of_isCompact (isBounded_Ioo _ _).isCompact_closure <| Continuous.continuousOn <| by fun_prop).symm

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