equivalence_join — Mathlib

English

If r is reflexive and transitive and the joining condition holds, then Join r is an equivalence relation.

Русский

Если r рефлексивно, транзитивно и выполняется условие соединения, тогда Join r является отношением эквивалентности.

LaTeX

$$$\\\\operatorname{Equivalence}(\\\\operatorname{Join} r)$$$

Lean4

theorem equivalence_join (hr : Reflexive r) (ht : Transitive r) (h : ∀ a b c, r a b → r a c → Join r b c) :
    Equivalence (Join r) :=
  ⟨reflexive_join hr, @symmetric_join _ _, @transitive_join _ _ ht h⟩

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