isCountablyGenerated_principal

Mathlib.Order.Filter.CountablyGenerated

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

← MathLib Explorer

English

For any set s, the principal filter 𝓟 s is countably generated.

Русский

Для любого множества s фильтр principals 𝓟 s счетно-порожден.

LaTeX

$$$\\operatorname{IsCountablyGenerated}(\\mathcal{P}(s))$$$

Lean4

@[instance]
theorem isCountablyGenerated_principal (s : Set α) : IsCountablyGenerated (𝓟 s) :=
  isCountablyGenerated_of_seq ⟨fun _ => s, iInf_const.symm⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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