symm — Mathlib

English

If d is a disjoint relation between l1 and l2, then it is also disjoint with the roles reversed: Disjoint l2 l1.

Русский

Если d является отношением несоприкасаемости между l1 и l2, то оно же несоприкасательно и для л2 и l1.

LaTeX

$$$$ \\forall l_1\\, l_2\\, (d:\\mathrm{Disjoint}\\, l_1\\, l_2) \\Rightarrow (\\mathrm{Disjoint}\\, l_2\\, l_1). $$$$

Lean4

@[symm]
theorem symm (d : Disjoint l₁ l₂) : Disjoint l₂ l₁ := fun _ i₂ i₁ => d i₁ i₂

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