countableBasis — Mathlib

English

countableBasis α is a countable set of subsets of α chosen from a second-countable topology; it serves as a basis source.

Русский

countableBasis α — это счётное множество подмножеств α, отобранное из второй счётности; служит источником базиса.

LaTeX

$$$\text{countableBasis}(\alpha)$ is a subset of $\mathcal P(\alpha)$ with countable cardinality generating the topology$$

Lean4

/-- A countable topological basis of `α`. -/
def countableBasis [SecondCountableTopology α] : Set (Set α) :=
  (exists_countable_basis α).choose

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