top_mem

Mathlib.Order.PFilter

URI: https://scilib.ai/kg/mathlib#Order.PFilter.top_mem

English

If P has a top element, then top belongs to every PFilter.

Русский

Если у P есть верхняя грань, то верхний элемент принадлежит каждому PFilter.

LaTeX

$$$$ \\top \\in F. $$$$

Lean4

/-- A specific witness of `pfilter.nonempty` when `P` has a top element. -/
@[simp]
theorem top_mem : ⊤ ∈ F :=
  Ideal.bot_mem _

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

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

Разделы

Аффилиация

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