decide — Mathlib

English

If r is trichotomous and we define r′ by decide(r(a,b)) = true, then r′ is trichotomous: for any a,b, r′(a,b) ∨ a = b ∨ r′(b,a).

Русский

Если r тричотомично, то r′(a,b) ⇔ decide(r(a,b)) = true; тогда r′ тричотомично: для любых a,b выполняется r′(a,b) ∨ a = b ∨ r′(b,a).

LaTeX

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

Lean4

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

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