English
Let α be a space with OrderTopology. For a map f: β → α, f is continuous iff for every a ∈ α, both f⁻¹(Ioi(a)) and f⁻¹(Iio(a)) are open in β.
Русский
Пусть у пространства α есть топология порядка. Тогда отображение f: β → α непрерывно тогда и только тогда, когда для каждого a ∈ α множества f⁻¹(Ioi(a)) и f⁻¹(Iio(a)) открыты в β.
LaTeX
$$$\\text{Continuous}(f) \\iff \\forall a, \\; \\text{IsOpen}(f^{-1}(Ioi(a))) \\ \\land \\ \\text{IsOpen}(f^{-1}(Iio(a)))$$$
Lean4
protected theorem continuous_iff [OrderTopology α] [TopologicalSpace β] {f : β → α} :
Continuous f ↔ ∀ a, IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a) :=
by
simp_rw [OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff]
aesop
