nonempty_sets

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#FilterBasis.nonempty_sets

English

A filter basis on α has a nonempty family of sets, i.e., its defining collection is nonempty.

Русский

Базис фильтра на α имеет ненулерьную семью множеств, то есть определяющая коллекция непуста.

LaTeX

$$$\operatorname{Nonempty} (B.\text{sets})$$$

Lean4

instance nonempty_sets (B : FilterBasis α) : Nonempty B.sets :=
  B.nonempty.to_subtype

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

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

Разделы

Аффилиация

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