Theorems · Theorem · order theory

Set.image2_union_left

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  Set.image2 f (s ∪ s') t = Set.image2 f s t ∪ Set.image2 f s' t

Defined in: Mathlib.Data.Set.NAry
Cited by: 14 results in Mathlib
Foundations: Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.imageproof · cited by 5,609
SProd.sprodproof · cited by 1,750
Set.image2statement · cited by 311
Set.image_unionproof · cited by 48
Set.union_prodproof · cited by 4

Cited by14

Results whose statement or proof uses this declaration.

Set.image2_union_rightproof · cited by 13
Finset.image₂_union_leftproof · cited by 10
Set.image2_union_inter_subset_unionproof · cited by 9
Set.union_mulproof · cited by 4
Set.union_addproof · cited by 3
Set.image2_insert_leftproof · cited by 1
Set.infs_union_leftproof · cited by 0
Set.union_divproof · cited by 0
Set.union_vaddproof · cited by 0
Set.union_vsubproof · cited by 0
Set.union_sdivproof · cited by 0
Set.union_smulproof · cited by 0