toContinuousLinearEquivOfBounds — Mathlib

English

A linear equivalence with both directional bounds induces a continuous linear equivalence.

Русский

Линейное эквивалентное отображение с двумя ограничениями порождает непрерывное линейное эквивалентное отображение.

LaTeX

$$$e: E \simeq_σ F$ with bounds $C_{to}, C_{inv}$ yields $E \simeq^{{σ}} F$ as a continuous linear equivalence$$

Lean4

/-- Construct a continuous linear equivalence from a linear equivalence together with
bounds in both directions. -/
def toContinuousLinearEquivOfBounds (e : E ≃ₛₗ[σ] F) (C_to C_inv : ℝ) (h_to : ∀ x, ‖e x‖ ≤ C_to * ‖x‖)
    (h_inv : ∀ x : F, ‖e.symm x‖ ≤ C_inv * ‖x‖) : E ≃SL[σ] F
    where
  toLinearEquiv := e
  continuous_toFun := AddMonoidHomClass.continuous_of_bound e C_to h_to
  continuous_invFun := AddMonoidHomClass.continuous_of_bound e.symm C_inv h_inv

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