ordConnected — Mathlib

English

If s is an antichain (with respect to ≤) then s is OrdConnected.

Русский

Если множество s является антицепной подмножностью относительно порядка ≤, то оно упорядоченно связно.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, s) \\Rightarrow \\operatorname{OrdConnected}(s)$$$

Lean4

protected theorem _root_.IsAntichain.ordConnected (hs : IsAntichain (· ≤ ·) s) : s.OrdConnected :=
  ⟨fun x hx y hy z hz => by
    obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
    rw [Icc_self, mem_singleton_iff] at hz
    rwa [hz]⟩

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