forall_eq_of_chain — Mathlib

English

If r is transitive and antisymmetric, and s forms a Chain under r, then every two elements of s are equal.

Русский

Если r транзитивно и антисимметрично, и s образует цепь, то любые два элемента s равны друг другу.

LaTeX

$$$$ [IsTrans\\;\\alpha\\;r] [IsAntisymm\\;\\alpha\\;r] (hs : Chain\\ r\\ s) \\Rightarrow \\forall a\\in s, \\forall b \\in s, a = b. $$$$

Lean4

theorem forall_eq_of_chain [IsTrans α r] [IsAntisymm α r] (hs : Chain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    a = b := by
  rw [chain_iff_pairwise] at hs
  exact antisymm (hs a ha b hb) (hs b hb a ha)

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