image₂_inter_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image₂_inter_left [DecidableEq α] (hf : Injective2 f) : image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t :=
  coe_injective <| by
    push_cast
    exact image2_inter_left hf

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