secondCountableTopology — Mathlib

English

If α and β are second countable, then WithLp p (α × β) is second countable.

Русский

Если пространства α и β вторично счётны, то WithLp p (α × β) вторично счётно.

LaTeX

$$$$\text{WithLp.secondCountableTopology }(p, α, β) : \text{SecondCountableTopology}(WithLp p (α × β))$$$$

Lean4

instance secondCountableTopology : SecondCountableTopology (WithLp p (α × β)) :=
  inferInstanceAs <| SecondCountableTopology (α × β)

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