eq — Mathlib · SciLib

English

If hs is a strong antichain on s, and {a ∈ s} and {b ∈ s} with a ≤ c and b ≤ c, then a = b.

Русский

Если s является сильной антицепью на s и a,b ∈ s имеют общий верхний предел c, то a = b.

LaTeX

$$$\\text{IsStrongAntichain}(r, s) \\Rightarrow \\forall a,b,c,\\ a \\in s \\land b \\in s \\land r a c \\land r b c \\Rightarrow a = b$$$

Lean4

theorem eq (hs : IsStrongAntichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c) (hbc : r b c) : a = b :=
  (Set.Pairwise.eq hs ha hb) fun h => False.elim <| (h c).elim (not_not_intro hac) (not_not_intro hbc)

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