iSup_range_single_le_iInf_ker_proj

English

The underlying function of the LinearMap.single is the Pi.single function.

Русский

Функциональная оболочка LinearMap.single совпадает с Pi.single.

LaTeX

$$$\\operatorname{coe}(\\text{single } R \\; \\varphi \\; i) = \\Pi\\text{single}_i.$$$

Lean4

theorem iSup_range_single_le_iInf_ker_proj (I J : Set ι) (h : Disjoint I J) :
    ⨆ i ∈ I, range (single R φ i) ≤ ⨅ i ∈ J, ker (proj i : (∀ i, φ i) →ₗ[R] φ i) :=
  by
  refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_
  simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
  rintro b - j hj
  rw [proj_comp_single_ne R φ j i, zero_apply]
  rintro rfl
  exact h.le_bot ⟨hi, hj⟩

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