decidableLE — Mathlib

English

If α is a preorder with a decidable ≤, and p is a predicate on α, then the subtype {x ∈ α | p(x)} inherits the induced order, and the relation ≤ on the subtype is decidable.

Русский

Пусть α упорядочено и ≤ разрешимо, и p — предикат на α. Тогда подтип {x ∈ α | p(x)} наследует естественный порядок, и отношение ≤ на подтипе разрешимо.

LaTeX

$$$\operatorname{DecidableLE}\left\{ x \in \alpha \;|\; p(x) \right\}$$$

Lean4

instance decidableLE [Preorder α] [h : DecidableLE α] {p : α → Prop} : DecidableLE (Subtype p) := fun a b ↦ h a b

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