image2_eq_iUnion — Mathlib

English

The image2 of a function with a two-variable argument distributes as an iUnion: image2 f s t = ⋃_{i ∈ s} ⋃_{j ∈ t} { f(i,j) }.

Русский

Изображение пары значений образует двойной союз множеств.

LaTeX

$$$\text{image2}(f,s,t) = \bigcup_{i \in s} \bigcup_{j \in t} \{f(i,j)\}$$$

Lean4

/-- The `Set.image2` version of `Set.image_eq_iUnion` -/
theorem image2_eq_iUnion (s : Set α) (t : Set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j} := by ext; simp [eq_comm]

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