controlled_closure_range_of_complete

English

If the image of a homomorphism j has elements with a norm bound, the same bound extends to the closure of its range via a bounded preimage for f.

Русский

Если образ гомоморфизма j имеет элементы с ограниченной нормой, аналогичное ограничение распространяется на замыкание образа через соответствующий ограниченный предобраз.

LaTeX

$$$\\forall b \\in \\overline{j(Range)},\\exists a:\\mathbb{N}\\to E,\\ Tendsto \\big(\\prod_{i=0}^n j(a_i)\\big) \\to b$ and bounds $\|j(a_0)/b\|

Lean4

/-- 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).
-/
theorem controlled_closure_range_of_complete {f : NormedAddGroupHom G H} {K : Type*} [SeminormedAddCommGroup K]
    {j : NormedAddGroupHom K H} (hj : ∀ x, ‖j x‖ = ‖x‖) {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε)
    (hyp : ∀ k, ∃ g, f g = j k ∧ ‖g‖ ≤ C * ‖k‖) : f.SurjectiveOnWith j.range.topologicalClosure (C + ε) :=
  by
  replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖ :=
    by
    intro h h_in
    rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩
    rw [hj]
    exact hyp k
  exact controlled_closure_of_complete hC hε hyp

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