ker_le_ker_iff_range_le_range — Mathlib

English

If E is finite dimensional and T, U are symmetric operators on E, then ker U ≤ ker T if and only if range T ≤ range U.

Русский

Если E конечноразмерно, и T, U — симметрические операторы на E, то ker U ⊆ ker T тогда и только тогда, когда range T ⊆ range U.

LaTeX

$$ker U ≤ ker T iff range T ≤ range U$$

Lean4

theorem ker_le_ker_iff_range_le_range [FiniteDimensional 𝕜 E] {T U : E →L[𝕜] E} (hT : T.IsSymmetric)
    (hU : U.IsSymmetric) : LinearMap.ker U ≤ LinearMap.ker T ↔ LinearMap.range T ≤ LinearMap.range U :=
  by
  refine ⟨fun h ↦ ?_, LinearMap.ker_le_ker_of_range hT hU⟩
  have := FiniteDimensional.complete 𝕜 E
  simpa [orthogonal_ker, hT, hU] using Submodule.orthogonal_le h

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