English
Let α be a preorder. If a is related to b by antisymmetry of ≤, and c is related to d by antisymmetry of ≤, then a is incomparable with c if and only if b is incomparable with d.
Русский
Пусть α — частично упорядоченное множество. Пусть a и b связаны антисимметрическим отношением ≤, и c и d связаны аналогично; тогда a несопоставим с c тогда как b несопоставим с d.
LaTeX
$$$\\forall a\\ b\\ c\\ d, AntisymmRel(\\le) \\ a \\ b \\rightarrow AntisymmRel(\\le) \\ c \\ d \\rightarrow IncompRel(\\le) \\ a \\ c \\leftrightarrow IncompRel(\\le) \\ b \\ d$$$
Lean4
theorem incompRel_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
IncompRel (· ≤ ·) a c ↔ IncompRel (· ≤ ·) b d
where
mp h := (h₁.symm.trans_incompRel h).trans_antisymmRel h₂
mpr h := (h₁.trans_incompRel h).trans_antisymmRel h₂.symm
