English
From a linear map f and a bounded image of a neighborhood of 0, construct a continuous linear map that agrees with f on E.
Русский
Из линейного отображения f и ограниченного образа окрестности нуля построить непрерывное линейное отображение, совпадающее с f на всей области.
LaTeX
$$$\\text{clmOfExistsBoundedImage}(f,h): E \\to L_{\\mathbb{k}}(F)$ with \\(h: \\exists V \\in 𝓝(0), \\; Bornology.IsVonNBounded( f''V)\\) exists$$
Lean4
/-- Construct a continuous linear map from a linear map `f : E →ₗ[𝕜] F` and the existence of a
neighborhood of zero that gets mapped into a bounded set in `F`. -/
def clmOfExistsBoundedImage (f : E →ₗ[𝕜] F) (h : ∃ V ∈ 𝓝 (0 : E), Bornology.IsVonNBounded 𝕜 (f '' V)) : E →L[𝕜] F :=
⟨f, by
-- It suffices to show that `f` is continuous at `0`.
refine continuous_of_continuousAt_zero f ?_
rw [continuousAt_def, f.map_zero]
intro U hU
rcases h with ⟨V, hV, h⟩
rcases (h hU).exists_pos with ⟨r, hr, h⟩
rcases NormedField.exists_lt_norm 𝕜 r with ⟨x, hx⟩
specialize h x hx.le
have x_ne := norm_pos_iff.mp (hr.trans hx)
have : x⁻¹ • V ⊆ f ⁻¹' U :=
calc
x⁻¹ • V ⊆ x⁻¹ • f ⁻¹' (f '' V) := Set.smul_set_mono (Set.subset_preimage_image (⇑f) V)
_ ⊆ x⁻¹ • f ⁻¹' (x • U) := (Set.smul_set_mono (Set.preimage_mono h))
_ = f ⁻¹' (x⁻¹ • x • U) := by
ext
simp only [Set.mem_inv_smul_set_iff₀ x_ne, Set.mem_preimage, LinearMap.map_smul]
_ ⊆ f ⁻¹' U := by
rw [inv_smul_smul₀ x_ne _]
-- Using this inclusion, it suffices to show that `x⁻¹ • V` is in `𝓝 0`, which is trivial.
refine mem_of_superset ?_ this
rwa [set_smul_mem_nhds_zero_iff (inv_ne_zero x_ne)]⟩
