symmetric_join — Mathlib

English

The Join relation is symmetric: if Join r a b holds then Join r b a holds with the same witness.

Русский

Отношение Join r симметрично: если существует путь от a к b через r, то существует путь обратно от b к a.

LaTeX

$$$\\\\forall a b, \\\\operatorname{Join} r a b \\\\Rightarrow \\\\operatorname{Join} r b a$$$$

Lean4

theorem symmetric_join : Symmetric (Join r) := fun _ _ ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩

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