equivalence_join_reflTransGen — Mathlib

English

If h ensures join for ReflTransGen r, then Join (ReflTransGen r) is an equivalence.

Русский

Если существует способ объединить через ReflTransGen r, то Join (ReflTransGen r) образует эквивалентность.

LaTeX

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

Lean4

theorem equivalence_join_reflTransGen (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) :
    Equivalence (Join (ReflTransGen r)) :=
  equivalence_join reflexive_reflTransGen transitive_reflTransGen fun _ _ _ ↦ church_rosser h

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