instDecidablePredMemUpperClosure — Mathlib

English

Definition of an instance providing decidability for upperClosure membership from a decidable predicate on ∃ a ∈ s, a ≤ x.

Русский

Определение экземпляра, обеспечивающего разрешимость членства в верхнем замыкании при разрешимости предиката на ∃ a ∈ s, a ≤ x.

LaTeX

$$[DecidablePred (∃ a ∈ s, a ≤ x)] → DecidablePred (x ∈ upperClosure s)$$

Lean4

instance instDecidablePredMemUpperClosure [DecidablePred (∃ a ∈ s, a ≤ ·)] : DecidablePred (· ∈ upperClosure s) :=
  ‹DecidablePred _›

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