transitive_join — Mathlib

English

If r is transitive and every pair of joins from a common source can be joined, then Join r is transitive.

Русский

Если r транзитивно и для любых a,b,c выполняется условие соединения, то Join r является транзитивным.

LaTeX

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

Lean4

theorem transitive_join (ht : Transitive r) (h : ∀ a b c, r a b → r a c → Join r b c) : Transitive (Join r) :=
  fun _ b _ ⟨x, hax, hbx⟩ ⟨y, hby, hcy⟩ ↦
  let ⟨z, hxz, hyz⟩ := h b x y hbx hby
  ⟨z, ht hax hxz, ht hcy hyz⟩

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