instDecidablePredMemLowerClosure

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#instDecidablePredMemLowerClosure

English

If the predicate ∃ a ∈ s, x ≤ a is decidable, then x ∈ lowerClosure s is decidable.

Русский

Если предикат ∃ a ∈ s, x ≤ a разрешим, то x ∈ lowerClosure s разрешимо.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru