instSecondCountableTopologyOrderDual

English

If α has a second-countable topology, then its order dual αᵒᵈ also has a second-countable topology.

Русский

Если у пространства с топологией есть второй счетный базис, то у его двойственного порядка αᵒᵈ тоже имеется вторый счетный базис.

LaTeX

$$$[TopologicalSpace\, \alpha]\ [SecondCountableTopology\, \alpha]\Rightarrow SecondCountableTopology\, (OrderDual\, \alpha).$$$

Lean4

instance [TopologicalSpace α] [h : SecondCountableTopology α] : SecondCountableTopology αᵒᵈ :=
  h

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