instFirstCountableTopologyOrderDual

English

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

Русский

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

LaTeX

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

Lean4

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

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