English
There exists a C such that for all u and finite index sets, a bound holds: opNNNorm ≤ C·M with appropriate M.
Русский
Существует C, такой что для всех u и конечных индексов существует предел: opNNNorm ≤ C·M.
LaTeX
$$$\exists C>0,\, \text{opNNNorm}(u) ≤ C\cdot M$$$
Lean4
/-- The set of injective continuous linear maps `E → F` is open,
if `E` is finite-dimensional over a complete field. -/
theorem isOpen_injective [FiniteDimensional 𝕜 E] : IsOpen {L : E →L[𝕜] F | Injective L} :=
by
rw [isOpen_iff_eventually]
rintro φ₀ hφ₀
rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩
have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_pos
filter_upwards [this] with φ hφ
apply φ.injective_iff_antilipschitz.mpr
exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ), H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩
