above_mem

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Cofinal.above_mem

English

The element produced by above lies in D.

Русский

Элемент, полученный через above, принадлежит D.

LaTeX

$$$ D.above x \in D. $$$

Lean4

theorem above_mem : D.above x ∈ D :=
  (Classical.choose_spec <| D.isCofinal x).1

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

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

Разделы

Аффилиация

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