English
For an IsQuotient map f, for any ε > 0 and any n ∈ N, there exists m ∈ M with f(m) = n and ‖m‖ < ‖n‖ + ε.
Русский
Для отображения, являющегося сюрьектом, существует предобраз с малой нормой: ∃m: M, f(m)=n и ‖m‖ < ‖n‖+ε.
LaTeX
$$$\\exists m : M, f m = n \\land ‖m‖ < ‖n‖ + ε$$$
Lean4
theorem norm_lift {f : NormedAddGroupHom M N} (hquot : IsQuotient f) {ε : ℝ} (hε : 0 < ε) (n : N) :
∃ m : M, f m = n ∧ ‖m‖ < ‖n‖ + ε := by
obtain ⟨m, rfl⟩ := hquot.surjective n
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty :=
by
rw [Set.image_nonempty]
exact ⟨0, f.ker.zero_mem⟩
rcases Real.lt_sInf_add_pos nonemp hε with
⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by rwa [hquot.norm]⟩
