sInter_image2 — Mathlib

English

Let f be a function α → β → Set γ and s ⊆ α, t ⊆ β. The intersection of image2 f s t equals the intersection 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

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

Lean4

@[simp]
theorem sInter_image2 (f : α → β → Set γ) (s : Set α) (t : Set β) : ⋂₀ (image2 f s t) = ⋂ (a ∈ s) (b ∈ t), f a b :=
  sInf_image2

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