Theorems · Theorem · functional analysis

Submodule.Quotient.norm_mk_lt

∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {R : Type u_3} [inst_1 : Ring R] [inst_2 : Module R M]
  {S : Submodule R M} (x : M ⧸ S) {ε : ℝ}, 0 < ε → ∃ m, Submodule.Quotient.mk m = x ∧ ‖m‖ < ‖x‖ + ε

For any x : M ⧸ S and any 0 < ε, there is m : M such that Submodule.Quotient.mk m = x and ‖m‖ < ‖x‖ + ε.

Defined in

Mathlib.Analysis.Normed.Group.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupRingModule