of_subsingleton

Mathlib.Order.Filter.Subsingleton

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

English

If α is a Subsingleton type, then any filter l on α is subsingleton.

Русский

Если тип α является подсинглетным, то любой фильтр l над α является подсинглетным.

LaTeX

$$$[Subsingleton \alpha] \Rightarrow l.Subsingleton$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] : l.Subsingleton :=
  ⟨univ, univ_mem, subsingleton_univ⟩

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

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

Разделы

Аффилиация

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