decide — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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