mono — Mathlib

English

If a morphism has the SurjectiveOnWith property with bound C, and C ≤ C', then it also has the property with bound C'.

Русский

Если тождественный морфизм обладает свойством SurjectiveOnWith при константе C и C ≤ C', то он обладает этим же свойством и при C'.

LaTeX

$$$ f.SurjectiveOnWith\\ K\\ C \\to f.SurjectiveOnWith\\ K\\ C' $ при условии $C ≤ C'$$$

Lean4

theorem mono {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C C' : ℝ} (h : f.SurjectiveOnWith K C) (H : C ≤ C') :
    f.SurjectiveOnWith K C' := by
  intro k k_in
  rcases h k k_in with ⟨g, rfl, hg⟩
  use g, rfl
  by_cases Hg : ‖f g‖ = 0
  · simpa [Hg] using hg
  · exact hg.trans (by gcongr)

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