English
Let f: α → β between preordered topological spaces with upper-set structure. Then f is monotone if and only if f is continuous.
Русский
Пусть f: α → β между пространствами с предorder и топологией верхних множеств. Тогда f монотонна тогда и только тогда, когда она непрерывна.
LaTeX
$$$$ \\text{Monotone}(f) \\iff \\text{Continuous}(f). $$$$
Lean4
protected theorem monotone_iff_continuous [TopologicalSpace α] [TopologicalSpace β] [Topology.IsUpperSet α]
[Topology.IsUpperSet β] {f : α → β} : Monotone f ↔ Continuous f :=
by
constructor
· intro hf
simp_rw [continuous_def, isOpen_iff_isUpperSet]
exact fun _ hs ↦ IsUpperSet.preimage hs hf
· intro hf a b hab
rw [← mem_Iic, ← closure_singleton] at hab ⊢
apply Continuous.closure_preimage_subset hf {f b}
apply mem_of_mem_of_subset hab
apply closure_mono
rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
