incompRel_compl — Mathlib

English

Let r be a binary relation on a type α. The incomparability relation with respect to the complement of r is exactly the antisymmetry relation of r; that is, for all a,b, IncompRel(rᶜ) a b holds iff AntisymmRel r a b.

Русский

Пусть r — бинарное отношение на множество α. Несопоставимость относительно дополнения rᶜ эквивалентна антисимметричности отношения r; то есть для любых a,b верно IncompRel(rᶜ) a b тогда и только тогда, когда AntisymmRel r a b.

LaTeX

$$$IncompRel(r^{c}) = AntisymmRel(r)$$$

Lean4

@[simp]
theorem incompRel_compl : IncompRel rᶜ = AntisymmRel r := by simp [← antisymmRel_compl, compl]

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