span_weight_isNonZero_eq_top — Mathlib

English

The span of nonzero weights images equals the top subspace.

Русский

Образ ненулевых весов порождает верхнее подполье.

LaTeX

$$$ span K (\\{ α : Weight K H L | α.IsNonZero \\}.image (Weight.toLinear K H L)) = \\top $$$

Lean4

@[simp]
theorem span_weight_isNonZero_eq_top : span K ({α : Weight K H L | α.IsNonZero}.image (Weight.toLinear K H L)) = ⊤ :=
  by
  rw [← span_weight_eq_top]
  refine le_antisymm (Submodule.span_mono <| by simp) ?_
  suffices range (Weight.toLinear K H L) ⊆ insert 0 ({α : Weight K H L | α.IsNonZero}.image (Weight.toLinear K H L)) by
    simpa only [Submodule.span_insert_zero] using Submodule.span_mono this
  rintro - ⟨α, rfl⟩
  simp only [mem_insert_iff, Weight.coe_toLinear_eq_zero_iff, mem_image, mem_setOf_eq]
  tauto

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