not_ordConnected_inter_Icc_iff — Mathlib

English

For x,y ∈ s, not OrdConnected(s ∩ Icc x y) is equivalent to the existence of z ∉ s with z ∈ Ioo x y.

Русский

Для x,y ∈ s не‑упорядоченно связное множество s ∩ Icc x y эквивалентно существованию z не в s, такого что z ∈ Ioo x y.

LaTeX

$$$x \\in s \\land y \\in s \\Rightarrow \\neg \\operatorname{OrdConnected}(s \\cap Icc(x,y)) \\iff \\exists z \\notin s,\\ z \\in Ioo(x,y)$$$

Lean4

theorem not_ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) : ¬OrdConnected (s ∩ Icc x y) ↔ ∃ z ∉ s, z ∈ Ioo x y :=
  by simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]

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