mem_top

Mathlib.Order.CompleteLattice.SetLike

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.mem_top

English

In a CompleteSublattice, the top element contains every x: x ∈ ⊤.

Русский

В полной подпредельной структуре верхний элемент содержит все x: x ∈ ⊤.

LaTeX

$$$x \\in (\\top : L)$$$

Lean4

@[simp]
theorem mem_top : x ∈ (⊤ : L) := by simp [← mem_subtype]

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

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

Разделы

Аффилиация

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