decide — Mathlib

English

If r is antisymmetric and we define r′ by decide(r(a,b)) = true, then r′ is antisymmetric: r′(a,b) and r′(b,a) imply a = b.

Русский

Если r антисимметрично и r′(a,b) ⇔ decide(r(a,b)) = true, то r′ антисимметрично: r′(a,b) и r′(b,a) приводят к a = b.

LaTeX

$$$\forall a,b:\alpha, (\mathrm{decide}(r\, a\, b) = \mathrm{true} \land \mathrm{decide}(r\, b\, a) = \mathrm{true}) \rightarrow a = b$$$

Lean4

instance decide [DecidableRel r] [IsAntisymm α r] : IsAntisymm α (fun a b => decide (r a b) = true) where
  antisymm a b h₁ h₂ := antisymm (r := r) _ _ (by simpa using h₁) (by simpa using h₂)

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