image_sigma_eq_iUnion

Mathlib.Data.Set.Sigma

URI: https://scilib.ai/kg/mathlib#Set.image_sigma_eq_iUnion

English

If each t(i) is nonempty, then fst image of s.sigma t equals s.

Русский

Если для каждого i множество t(i) непусто, то образ fst сигмы равен s.

LaTeX

$$$ \\Sigma^{\\mathrm{fst}} '' (s \\sigma t) = s \\quad \\text{if } \\forall i, (t(i)) \\neq \\emptyset $$$

Lean4

theorem image_sigma_eq_iUnion {γ : Type*} (f : (Σ i, α i) → γ) : f '' (s.sigma t) = ⋃ i ∈ s, (f ∘ Sigma.mk i) '' t i :=
  by aesop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru