orthogonal_span_singleton_eq_to_lin_ker

English

The orthogonalBilin of the span of x equals the kernel of B x.

Русский

Ортогональная билинейная часть пространства, порожденного единичным вектором x, равна ядру линейного отображения B x.

LaTeX

$$$(\text{span}(K∗x)^{⊥_B}) = \ker(B x)$$$

Lean4

theorem orthogonal_span_singleton_eq_to_lin_ker {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V) :
    Submodule.orthogonalBilin (K ∙ x) B = LinearMap.ker (B x) :=
  by
  ext y
  simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
  constructor
  · exact fun h ↦ h x ⟨1, one_smul _ _⟩
  · rintro h _ ⟨z, rfl⟩
    rw [isOrtho_def, map_smulₛₗ₂, smul_eq_zero]
    exact Or.intro_right _ h

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