instIsBoundedSMul — Mathlib

English

For any m, the norm of mk m is bounded by the norm of m.

Русский

Для любого m норма mk(m) ограничена нормой m.

LaTeX

$$$\\|Submodule.Quotient.mk m\\| \\le \\|m\\|$$$

Lean4

instance instIsBoundedSMul (𝕜 : Type*) [SeminormedCommRing 𝕜] [Module 𝕜 M] [IsBoundedSMul 𝕜 M] [SMul 𝕜 R]
    [IsScalarTower 𝕜 R M] : IsBoundedSMul 𝕜 (M ⧸ S) :=
  .of_norm_smul_le
    fun k x =>
      -- this is `QuotientAddGroup.norm_lift_apply_le` for `f : M → M ⧸ S` given by
          -- `x ↦ mk (k • x)`; todo: add scalar multiplication as `NormedAddGroupHom`, use it here

    _root_.le_of_forall_pos_le_add fun ε hε =>
      by
      have :=
        (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp
          ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε
      simp only [mem_ball, dist, abs_sub_lt_iff] at this
      rcases this with ⟨δ, hδ, h⟩
      obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ
      specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩
      calc
        _ ≤ ‖k‖ * ‖a‖ := (norm_mk_le ..).trans (norm_smul_le k a)
        _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

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