image₂_insert_right — Mathlib

English

image₂ f (insert a s) t = (t.image (\\lambda b. f a b)) ∪ image₂ f s t.

Русский

image₂ f (insert a s) t = (t.image (λ b. f a b)) ∪ image₂ f s t.

LaTeX

$$$\\operatorname{image}_2 f (\\operatorname{insert} a\\, s)\\, t = (t.\\operatorname{image} (\\\\lambda b. f a b)) \\cup \\operatorname{image}_2 f s t$$$

Lean4

@[simp]
theorem image₂_insert_right [DecidableEq β] : image₂ f s (insert b t) = (s.image fun a => f a b) ∪ image₂ f s t :=
  coe_injective <| by
    push_cast
    exact image2_insert_right

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