Theorems · Theorem · functional analysis

controlled_closure_range_of_complete

∀ {G : Type u_1} [inst : NormedAddCommGroup G] [CompleteSpace G] {H : Type u_2} [inst_2 : NormedAddCommGroup H]
  {f : NormedAddGroupHom G H} {K : Type u_3} [inst_3 : SeminormedAddCommGroup K] {j : NormedAddGroupHom K H},
  (∀ (x : K), ‖j x‖ = ‖x‖) →
    ∀ {C ε : ℝ},
      0 < C →
        0 < ε → (∀ (k : K), ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖) → f.SurjectiveOnWith j.range.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G, if every element x of the image of an isometric immersion j : NormedAddGroupHom K H has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of this image with constant C+ε instead of C, for any positive ε. This is useful in particular if j is the inclusion of a normed group into its completion (in this case the closure is the full target group).

Defined in

Mathlib.Analysis.Normed.Group.ControlledClosure

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupCompleteSpaceNormedAddCommGroupSeminormedAddCommGroup