ker_eq_bot — Mathlib

English

If a coercive operator B has an inverse in the Lax-Milgram setting, then its kernel is trivial; the only vector mapped to zero by B♯ is zero.

Русский

Для коэрцитивного отображения в рамках теоремы Лакса–Мильграма, его ядро тривиально: единственный вектор, который отображается в нуль, — нуль сам.

LaTeX

$$$ \ker B♯ = \{0\}. $$$

Lean4

theorem ker_eq_bot (coercive : IsCoercive B) : ker B♯ = ⊥ :=
  by
  rw [LinearMapClass.ker_eq_bot]
  rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
  exact antilipschitz.injective

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