ordConnected_inter_Icc_of_subset — Mathlib

English

If Ioo x y ⊆ s, then s ∩ Icc x y is OrdConnected.

Русский

Если Ioo(x,y) ⊆ s, то s ∩ Icc(x,y) упорядоченно связно.

LaTeX

$$$Ioo(x,y) \\subseteq s \\Rightarrow \\operatorname{OrdConnected}(s \\cap Icc(x,y))$$$

Lean4

theorem ordConnected_inter_Icc_of_subset (h : Ioo x y ⊆ s) : OrdConnected (s ∩ Icc x y) :=
  ordConnected_of_Ioo fun _u ⟨_, hu, _⟩ _v ⟨_, _, hv⟩ _ ↦
    Ioo_subset_Ioo hu hv |>.trans <| subset_inter h Ioo_subset_Icc_self

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