openSegment_subset_iff_segment_subset

English

If x ∈ s and y ∈ s, then openSegment 𝕜 x y ⊆ s if and only if the segment [x -[𝕜] y] ⊆ s.

Русский

Если x и y принадлежат s, то открытый сегмент между x и y ⊆ s тогда как лишь если сегмент между x и y ⊆ s.

LaTeX

$$$openSegment \\, 𝕜\\, x\\, y \\subseteq s \\iff [x -[𝕜] y] \\subseteq s$$$

Lean4

theorem openSegment_subset_iff_segment_subset (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s := by
  simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

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