secondCountableTopologyEither_of_right

English

If β has second-countable topology then SecondCountableTopologyEither α β holds.

Русский

Если β обладает второй счётной топологией, то выполняется SecondCountableTopologyEither α β.

LaTeX

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

Lean4

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

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