separatingLeft_iff_linear_nontrivial

English

A left-separating bilinear form has trivial left kernel; equivalently, ker B contains only 0.

Русский

Лево-разделяющая билинейная форма имеет тривиальное ядро слева; эквивалентно тому, что ker B = {0}.

LaTeX

$$$B.SeparatingLeft \\leftrightarrow \\ker B = \\{0\\}$$$

Lean4

theorem separatingLeft_iff_linear_nontrivial {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.SeparatingLeft ↔ ∀ x : M₁, B x = 0 → x = 0 :=
  by
  constructor <;> intro h x hB
  · simpa only [hB, zero_apply, eq_self_iff_true, forall_const] using h x
  have h' : B x = 0 := by
    ext
    rw [zero_apply]
    exact hB _
  exact h x h'

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