surjOn_Ioo_of_monotone_surjective

English

If f is monotone and surjective, then for any a,b, SurjOn f (Ico a b) (Ico(f a) (f b)).

Русский

Если f монотонна и сюрьективна, то для любых a,b выполняется SurjOn f (Ico a b) (Ico(f a) (f b)).

LaTeX

$$$\operatorname{SurjOn} f\ (\mathrm{Ico}\ a\ b)\ (\mathrm{Ico}\ (f a)\ (f b))$$$

Lean4

theorem surjOn_Ioo_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f) (a b : α) :
    SurjOn f (Ioo a b) (Ioo (f a) (f b)) := by
  intro p hp
  rcases h_surj p with ⟨x, rfl⟩
  refine ⟨x, mem_Ioo.2 ?_, rfl⟩
  contrapose! hp
  exact fun h => h.2.not_ge (h_mono <| hp <| h_mono.reflect_lt h.1)

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