decidableLT — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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