ordConnected_inter_Icc_iff — Mathlib

English

For x,y ∈ s, OrdConnected(s ∩ Icc x y) if and only if Ioo x y ⊆ s.

Русский

Для x,y ∈ s верно: OrdConnected( s ∩ Icc(x,y) ) тогда и только тогда, когда Ioo(x,y) ⊆ s.

LaTeX

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

Lean4

theorem ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) : OrdConnected (s ∩ Icc x y) ↔ Ioo x y ⊆ s :=
  by
  refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
  have hxy : x ≤ y := hz.1.trans hz.2
  exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

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