ker_le_ker_of_range — Mathlib

English

If S and T are symmetric and range S ⊆ range T, then ker T ⊆ ker S.

Русский

Если S и T симметричны и образ S вложен в образ T, то ядро T вложено в ядро S.

LaTeX

$$$ \ker T \subseteq \ker S $ under $S$ and $T$ symmetric and $\operatorname{range} S \le \operatorname{range} T$$$

Lean4

theorem ker_le_ker_of_range {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hT : T.IsSymmetric) (h : range S ≤ range T) :
    ker T ≤ ker S := by
  intro v hv
  rw [mem_ker] at hv ⊢
  obtain ⟨y, hy⟩ : ∃ y, T y = S (S v) := by simpa using @h (S (S v))
  rw [← inner_self_eq_zero (𝕜 := 𝕜), ← hS, ← hy, hT, hv, inner_zero_right]

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