monotone_to_lowerTopology_continuous

English

In the lower-set topology, monotone maps are continuous; thus monotone implies continuous for IsLowerSet spaces.

Русский

Во второй топологии нижних множеств монотонные отображения непрерывны; монотонность влечет непрерывность.

LaTeX

$$$$ \\text{Monotone}(f) \\Rightarrow \\text{Continuous}(f). $$$$

Lean4

theorem monotone_to_lowerTopology_continuous [TopologicalSpace α] [TopologicalSpace β] [Topology.IsLowerSet α]
    [IsLower β] {f : α → β} (hf : Monotone f) : Continuous f :=
  IsUpperSet.monotone_to_upperTopology_continuous (α := αᵒᵈ) (β := βᵒᵈ) hf.dual

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