le_comap_single_pi — Mathlib

English

For DecidableEq ι, iSup over i of map(single i) (p_i) is contained in pi I p.

Русский

Для декидируемого равенства индексов ι, iSup по i от map(single i) (p_i) ⊆ pi I p.

LaTeX

$$$$\\bigvee_i \\mathrm{map}(\\mathrm{single}_i)(p_i) \\le \\pi I p.$$$$

Lean4

theorem le_comap_single_pi [DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {I i} :
    p i ≤ Submodule.comap (LinearMap.single R φ i : φ i →ₗ[R] _) (Submodule.pi I p) :=
  by
  intro x hx
  rw [Submodule.mem_comap, Submodule.mem_pi]
  rintro j -
  rcases eq_or_ne j i with rfl | hne <;> simp [*]

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