segment_subset_closure_openSegment

English

In a suitable linear space over a linearly ordered ring, the closed segment from x to y is contained in the closure of the open segment between x and y.

Русский

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

LaTeX

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

Lean4

theorem segment_subset_closure_openSegment : [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y) :=
  by
  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
  exact image_closure_subset_closure_image (by fun_prop)

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