Theorems · Theorem · functional analysis

controlled_closure_of_complete

∀ {G : Type u_1} [inst : NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [inst_2 : NormedAddCommGroup H]
  {f : NormedAddGroupHom G H} {K : AddSubgroup H} {C ε : ℝ},
  0 < C → 0 < ε → f.SurjectiveOnWith K C → f.SurjectiveOnWith K.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G and a subgroup K of H, if every element x of K has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of K with constant C+ε instead of C, for any positive ε.

Defined in

Mathlib.Analysis.Normed.Group.ControlledClosure

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupCompleteSpaceNormedAddCommGroup