isClosed_range — Mathlib

English

The Lax-Milgram construction provides a continuous linear equivalence between the space and itself induced by a coercive bilinear form.

Русский

Построение Лакс–Мильграма задаёт непрерывное линейное эквивалентство на пространстве, соответствующее коэрцитивной билинейной форме.

LaTeX

$$$ \text{continuousLinearEquivOfBilin}(B) : V \simeq V. $$$

Lean4

theorem isClosed_range (coercive : IsCoercive B) : IsClosed (range B♯ : Set V) :=
  by
  rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
  exact antilipschitz.isClosed_range B♯.uniformContinuous

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