decide — Mathlib

English

If r is transitive and we define r′ by decide(r(a,b)) = true, then r′ is transitive: r′(a,b) and r′(b,c) imply r′(a,c).

Русский

Если r транзитивно и r′(a,b) ⇔ decide(r(a,b)) = true, то r′ транзитивно: если r′(a,b) и r′(b,c), то r′(a,c).

LaTeX

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

Lean4

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

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