biUnion_image_right — Mathlib

English

Symmetrically, t.biUnion (s.image ∘ f) = image₂ f s t.

Русский

Аналогично, правая биобъединенная операция равна образу двумя аргументами: t.biUnion (s.image ∘ f) = image₂ f s t.

LaTeX

$$$\mathrm{biUnion}\ t\ (\\lambda b. \mathrm{image}_2\ f s\\ b) = \mathrm{image}_2\ f s t$$$

Lean4

theorem biUnion_image_right : (t.biUnion fun b => s.image fun a => f a b) = image₂ f s t :=
  coe_injective <| by
    push_cast
    exact Set.iUnion_image_right _

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