English
If a continuous f on s has tendsto from both ends (dual tweaks), then f maps s onto all of δ.
Русский
Если непрерывная function на s имеет стремление к обоим концам, то образ \(f\) охватывает всю область значений.
LaTeX
$$SurjOn f s univ$$
Lean4
theorem strictMono_of_inj_boundedOrder [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊥ ≤ f ⊤)
(hf_i : Injective f) : StrictMono f := by
intro a b hab
by_contra! h
have H : f b < f a := lt_of_le_of_ne h <| hf_i.ne hab.ne'
by_cases ha : f a ≤ f ⊥
· obtain ⟨u, hu⟩ := intermediate_value_Ioc le_top hf_c.continuousOn ⟨H.trans_le ha, hf⟩
have : u = ⊥ := hf_i hu.2
simp_all
· by_cases hb : f ⊥ < f b
· obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
rw [hf_i hu.2] at hu
exact (hab.trans hu.1.2).false
· push_neg at ha hb
replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
have : u = ⊥ := hf_i hu.2
simp_all
