isCountablyGenerated — Mathlib

English

A subsingleton filter is countably generated.

Русский

Фильтр, обладающий свойством подсинглетности, является счётно порождаемым.

LaTeX

$$$$ l.Subsingleton \Rightarrow IsCountablyGenerated\ l $$$$

Lean4

theorem isCountablyGenerated (hl : l.Subsingleton) : IsCountablyGenerated l :=
  by
  rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩
  · exact isCountablyGenerated_bot
  · exact isCountablyGenerated_pure x

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