monotone_to_upperTopology_continuous

English

If f is monotone, then f is continuous with respect to the upper-set topology.

Русский

Если f монотонна, то она непрерывна в отношении топологии верхних множеств.

LaTeX

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

Lean4

theorem monotone_to_upperTopology_continuous [TopologicalSpace α] [TopologicalSpace β] [Topology.IsUpperSet α]
    [IsUpper β] {f : α → β} (hf : Monotone f) : Continuous f :=
  by
  simp_rw [continuous_def, isOpen_iff_isUpperSet]
  intro s hs
  exact (IsUpper.isUpperSet_of_isOpen hs).preimage hf

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