sUnion_image2 — Mathlib

English

Let f be a function α → β → Set γ and s ⊆ α, t ⊆ β. The union of image2 f s t equals the union over a ∈ s and b ∈ t of f(a,b): ⋃₀ (image2 f s t) = ⋃ (a ∈ s) (b ∈ t), f a b.

Русский

Пусть f: α → β → Set γ и s ⊆ α, t ⊆ β. Объединение image2 f s t равно объединению по всем a ∈ s и b ∈ t: ⋃₀ (image2 f s t) = ⋃ (a ∈ s) (b ∈ t), f a b.

LaTeX

$$$$ \\bigcup_{U \\in \\mathrm{image2}(f,s,t)} U = \\bigcup_{a \\in s} \\bigcup_{b \\in t} f(a,b). $$$$

Lean4

@[simp]
theorem sUnion_image2 (f : α → β → Set γ) (s : Set α) (t : Set β) : ⋃₀ (image2 f s t) = ⋃ (a ∈ s) (b ∈ t), f a b :=
  sSup_image2

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