decide — Mathlib

English

If r is reflexive, and we define a new relation by r′(a,b) holds when decide(r(a,b)) = true, then r′ is reflexive.

Русский

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

LaTeX

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

Lean4

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

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