secondCountableTopologyEither_of_left

English

If either α or β has a second-countable topology, then the product/union space inherits a second-countable topology (via either left or right instance).

Русский

Если хотя бы одно из пространств обладает счётной топологией, то в произведении сохраняется вторая счётность.

LaTeX

$$$SecondCountableTopologyEither \\alpha \\beta$.$$

Lean4

instance (priority := 100) secondCountableTopologyEither_of_left (α β : Type*) [TopologicalSpace α] [TopologicalSpace β]
    [SecondCountableTopology α] : SecondCountableTopologyEither α β where out := Or.inl (by infer_instance)

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