iSup_map_single — Mathlib

English

If the index type is finite, then the supremum over i of map(single i)(p_i) equals pi univ p.

Русский

Если множество индексов конечно, то верхняя грань по i от map(single i)(p_i) равна pi Set.univ p.

LaTeX

$$$$\\bigvee_i map(\\mathrm{single}_i)(p_i) = \\pi(\\mathrm{Set.univ}, p).$$$$

Lean4

theorem iSup_map_single [DecidableEq ι] [Finite ι] :
    ⨆ i, map (LinearMap.single R φ i : φ i →ₗ[R] (i : ι) → φ i) (p i) = pi Set.univ p :=
  by
  cases nonempty_fintype ι
  refine iSup_map_single_le.antisymm fun x hx => ?_
  rw [← Finset.univ_sum_single x]
  exact sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)

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