quotient_norm_mk_eq — Mathlib

English

For any S ≤ M and m ∈ M, and ε > 0 there exists s ∈ S with ∥m * s∥ < ∥mk' S m∥ + ε.

Русский

Для любых S ≤ M и m ∈ M и ε > 0 существует s ∈ S такое, что ∥m s∥ < ∥mk' S m∥ + ε.

LaTeX

$$$\exists s \in S, \; \|m * s\| < \|mk' S m\| + ε$$$

Lean4

/-- The norm of the image under the natural morphism to the quotient. -/
theorem quotient_norm_mk_eq (S : AddSubgroup M) (m : M) : ‖mk' S m‖ = sInf ((‖m + ·‖) '' S) :=
  by
  rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg_eq_neg, neg_coe_set (H := S),
    infDist_eq_iInf]
  simp only [dist_eq_norm', sub_neg_eq_add, add_comm]

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