atBot_neBot

Mathlib.Order.Filter.AtTopBot.Basic

URI: https://scilib.ai/kg/mathlib#Filter.atBot_neBot

English

There is a NeBot instance for atBot, mirroring atTop.

Русский

Существет NeBot для atBot, зеркально как и для atTop.

LaTeX

$$$ \\operatorname{atBot}.\\mathrm{NeBot} $$$

Lean4

@[instance]
theorem atBot_neBot : NeBot (atBot : Filter α) :=
  atTop_neBot (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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