of_segment_subset — Mathlib

English

If the real segment between x and y lies inside a set s, then x and y are joined in s by a path within s.

Русский

Если сегмент Real между точками x и y лежит в множестве s, то x и y соединены путём внутри s.

LaTeX

$$$ [x -[\mathbb{R}] y] \subseteq s \;\Rightarrow\; JoinedIn\ s\ x\ y $$$

Lean4

theorem of_segment_subset {x y : E} {s : Set E} (h : [x -[ℝ] y] ⊆ s) : JoinedIn s x y :=
  by
  use .segment x y
  rwa [← range_subset_iff, Path.range_segment]

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