range_polarizationIn_le_span_coroot

English

The range of PolarizationIn is contained in the coroot span.

Русский

Диапазон PolarizationIn содержится в коррет-охвате.

LaTeX

$$$\\operatorname{range}(P.Polarization In) \\le P.corootSpan S$$$

Lean4

theorem range_polarizationIn_le_span_coroot : LinearMap.range (P.PolarizationIn S) ≤ P.corootSpan S :=
  by
  intro x hx
  obtain ⟨y, hy⟩ := hx
  rw [PolarizationIn_apply] at hy
  exact (Submodule.mem_span_range_iff_exists_fun S).mpr (Exists.intro (fun i ↦ (P.coroot'In S i) y) hy)

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