decide — Mathlib

English

If r is asymmetric and we define r′ by decide(r(a,b)) = true, then r′ is asymmetric: r′(a,b) implies not r′(b,a).

Русский

Если r асимметрично и r′(a,b) ⇔ decide(r(a,b)) = true, то r′ асимметрично: r′(a,b) → ¬ r′(b,a).

LaTeX

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

Lean4

instance decide [DecidableRel r] [IsAsymm α r] : IsAsymm α (fun a b => decide (r a b) = true) where
  asymm := fun a b => by simpa using asymm a b

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