biUnion_image_left — Mathlib

English

The left hand biUnion of images coincides with the two-argument image: s.biUnion (t.image ∘ f) = image₂ f s t.

Русский

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

LaTeX

$$$\mathrm{biUnion}\ f\ s\ t = \mathrm{image}_2\ f\ s\ t$$$

Lean4

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

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