decide — Mathlib

English

If r is symmetric and we define r′ by decide(r(a,b)) = true, then r′ is symmetric: r′(a,b) implies 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 (\mathrm{decide}(r\, b\, a) = \mathrm{true})$$$

Lean4

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

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