mem_bot

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#UpperSet.mem_bot

English

The bottom UpperSet contains every element of α; i.e., a ∈ ⊥ for all a.

Русский

Нижнее верхнее множество содержит все элементы; для любого a верно a ∈ ⊥.

LaTeX

$$a ∈ \bot$$

Lean4

@[simp]
theorem mem_bot : a ∈ (⊥ : UpperSet α) :=
  trivial

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

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

Разделы

Аффилиация

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