atBot_basis

Mathlib.Order.Filter.AtTopBot.Basic

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

English

The atBot filter has a canonical basis given by all of α below, i.e., a true basis of Iic.

Русский

Фильтр atBot имеет канонический базис, задаваемый всеми элементами ниже, т. е. Iic.

LaTeX

$$$ \\operatorname{atBot.HasBasis} (\\textrm{True}) \\mathrm{Iic} $$$

Lean4

theorem atBot_basis : (@atBot α _).HasBasis (fun _ => True) Iic :=
  atTop_basis (α := αᵒᵈ)

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

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

Разделы

Аффилиация

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