iSup_map_single_le — Mathlib

English

Variant of the previous bound, with explicit DecidableEq ι assumptions.

Русский

Вариант предыдущего ограничения с явными предположениями DecidableEq ι.

LaTeX

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

Lean4

theorem iSup_map_single_le [DecidableEq ι] : ⨆ i, map (LinearMap.single R φ i) (p i) ≤ pi I p :=
  iSup_le fun _ => map_le_iff_le_comap.mpr <| le_comap_single_pi _

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