biInter_image2 — Mathlib

English

Let s ⊆ α, t ⊆ β, f: α → β → γ, g: γ → Set δ. Then ⋂ c ∈ image2 f s t, g c equals ⋂ a ∈ s, ⋂ b ∈ t, g(f a b).

Русский

Пусть s ⊆ α, t ⊆ β, f: α → β → γ, g: γ → Set δ. Тогда ⋂ c ∈ image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g(f a b).

LaTeX

$$$\bigcap_{c \in \operatorname{image2} f s t} g(c) = \bigcap_{a \in s} \bigcap_{b \in t} g(f(a,b))$$$

Lean4

theorem biInter_image2 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) :
    ⋂ c ∈ image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g (f a b) :=
  iInf_image2 ..

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