coe_lowerClosure

Mathlib.Order.UpperLower.Closure

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

English

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

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_lowerClosure (s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Iic a :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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