secondCountableTopology_source — Mathlib

English

If Y is second countable, then the source of an OpenPartialHomeomorph e: X → Y is also second countable.

Русский

Если Y второго счётного типа, то источник e: X → Y также второго счётного типа.

LaTeX

$$$[SecondCountableTopology Y] \Rightarrow SecondCountableTopology e.source$$$

Lean4

theorem secondCountableTopology_source [SecondCountableTopology Y] : SecondCountableTopology e.source :=
  e.toHomeomorphSourceTarget.secondCountableTopology

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