incompRel_compl_apply — Mathlib

English

For all a,b in α and relation r, IncompRel rᶜ a b is equivalent to AntisymmRel r a b.

Русский

Для любых a,b∈α и отношения r несопоставимость относительно дополнения rᶜ между a и b эквивалентна антисимметричности r между a и b.

LaTeX

$$$IncompRel(r^{c}) a b \leftrightarrow AntisymmRel(r) a b$$$

Lean4

@[simp]
theorem incompRel_compl_apply : IncompRel rᶜ a b ↔ AntisymmRel r a b := by simp

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