openSegment_interior_closure_subset_interior

English

If s is convex and x ∈ interior s, y ∈ closure s, then every point on the segment from x to y that lies in the open interval of s stays in interior(s).

Русский

Если S выпукло, x ∈ int(S), y ∈ closure(S), то любой точке на отрезке между x и y, лежащей внутри открытого сегмента, принадлежит interior(S).

LaTeX

$$$$\operatorname{openSegment}_{\mathbb{K}}(x,y) \subseteq \operatorname{Int}(s).$$$$

Lean4

theorem openSegment_interior_closure_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s)
    (hy : y ∈ closure s) : openSegment 𝕜 x y ⊆ interior s :=
  by
  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab

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