uIcc_subset — Mathlib

English

If s is OrdConnected, then for all x,y ∈ s, the uIcc x y is contained in s.

Русский

Если s упорядоченно связно, то для любых x,y∈s множество uIcc(x,y) ⊆ s.

LaTeX

$$$\\operatorname{OrdConnected}(s) \\Rightarrow \\forall x\\in s \\forall y\\in s, \\; \\operatorname{uIcc}(x,y) \\subseteq s$$$

Lean4

theorem uIcc_subset (hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) : [[x, y]] ⊆ s :=
  hs.out (min_rec' (· ∈ s) hx hy) (max_rec' (· ∈ s) hx hy)

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