mk' — Mathlib

English

Given a countable collection b of subsets of α, the topology generated by b is second-countable.

Русский

Дано счётное множество подмножеств b пространства α; топология, порождённая b, является второй счётной.

LaTeX

$$$\text{SecondCountableTopology}(\text{generateFrom}(b))$$$

Lean4

theorem mk' {α} {b : Set (Set α)} (hc : b.Countable) : @SecondCountableTopology α (generateFrom b) :=
  @SecondCountableTopology.mk α (generateFrom b) ⟨b, hc, rfl⟩

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