iSup_lsingle_range — Mathlib

English

The supremum of the ranges of all lsingle maps is the top submodule (i.e., they span the whole space).

Русский

Объединение образов всех lsingle—медленных покрывает всё пространство.

LaTeX

$$$\bigvee_{a} \operatorname{range}(\mathrm{lsingle} a) = \top$$$

Lean4

theorem iSup_lsingle_range : ⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M) = ⊤ :=
  by
  refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_
  rw [← sum_single f]
  exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

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