range_compLeft — Mathlib

English

Similarly, the range of the left-composition equals the product of ranges.

Русский

Аналогично: образ лево-композиции равен произведению образов.

LaTeX

$$$$\\mathrm{range}(f\\circ_{Left}I) = \\pi(\\mathrm{Set.univ}, \\mathrm{range} f).$$$$

Lean4

theorem range_compLeft [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (I : Type*) :
    LinearMap.range (f.compLeft I) = Submodule.pi (Set.univ : Set I) (fun _ => LinearMap.range f) :=
  Submodule.ext fun _ =>
    ⟨fun ⟨y, hy⟩ i _ => ⟨y i, congr_fun hy i⟩, fun hx =>
      by
      choose y hy using hx
      exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩⟩

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