coe_bot

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.coe_bot

English

The carrier of the bottom sublattice ⊥ is the empty set: the bottom sublattice has no elements.

Русский

Носитель нижней подрешетки ⊥ равен пустому множеству: нижняя подрешётка не содержит элементов.

LaTeX

$$$(\bot : \text{Sublattice } \alpha) = (\varnothing : \mathrm{Set} \alpha)$$$

Lean4

@[simp, norm_cast]
theorem coe_bot : (⊥ : Sublattice α) = (∅ : Set α) :=
  rfl

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

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

Разделы

Аффилиация

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