openSegment_closure_interior_subset_interior

English

If s is convex and x ∈ closure s, y ∈ interior s, then the open segment from x to y is contained in interior s.

Русский

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

LaTeX

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

Lean4

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

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