firstCountableTopology — Mathlib

English

If f is an embedding and β is first-countable, then α is first-countable.

Русский

Если f — вложение (эмбеддинг) и β имеет первую счётность, то и α имеет первую счётность.

LaTeX

$$$\text{FirstCountableTopology}(\alpha)$$$

Lean4

protected theorem _root_.Topology.IsEmbedding.firstCountableTopology {β : Type*} [TopologicalSpace β]
    [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) : FirstCountableTopology α :=
  hf.1.firstCountableTopology

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