atBot_eq

Mathlib.Order.Filter.AtTopBot.CompleteLattice

URI: https://scilib.ai/kg/mathlib#Filter.Subsingleton.atBot_eq

English

Similarly, for subsingleton α with a preorder, the atBot filter equals ⊤.

Русский

Аналогично, для subsingleton α с порядком, atBot = ⊤.

LaTeX

$$$$\text{If } [Subsingleton(\alpha)], [Preorder(\alpha)]\;:\; (\text{atBot} : \text{Filter } \alpha) = \top.$$$$

Lean4

@[nontriviality]
theorem atBot_eq (α) [Subsingleton α] [Preorder α] : (atBot : Filter α) = ⊤ :=
  @Subsingleton.atTop_eq αᵒᵈ _ _

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

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

Разделы

Аффилиация

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