sigma_insert — Mathlib

English

Let a be a family a(i) and t i be sets; then sigma with a(i) inserted into t(i) yields the union of (i, a(i)) over s with sigma t.

Русский

Пусть a(i) задаёт элемент в α(i) и t(i) множества; тогда сигма с добавлением a(i) в t(i) равна объединению (i, a(i)) для i ∈ s вместе с σ t.

LaTeX

$$$\bigcup_{i \in s} \bigcup_{j \in t(i) \cup \{a(i)\}} (i,j) = \{\langle i,a(i)\rangle : i \in s\} \cup (s \sigma t)$$$

Lean4

theorem sigma_insert {a : ∀ i, α i} : s.sigma (fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t := by
  grind

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