Theorems · Theorem · order theory

Set.image2_union_right

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

Defined in: Mathlib.Data.Set.NAry
Cited by: 13 results in Mathlib
Foundations: Depth 18 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.

Cites4

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.image2statement and proof · cited by 311
Set.image2_swapproof · cited by 17
Set.image2_union_leftproof · cited by 14

Cited by13

Results whose statement or proof uses this declaration.

Set.image2_inter_union_subset_unionproof · cited by 10
Finset.image₂_union_rightproof · cited by 10
Set.add_unionproof · cited by 2
Set.smul_unionproof · cited by 1
Set.image2_insert_rightproof · cited by 1
Set.mul_unionproof · cited by 1
Set.infs_union_rightproof · cited by 0
Set.vsub_unionproof · cited by 0
Set.div_unionproof · cited by 0
Set.vadd_unionproof · cited by 0
Set.sub_unionproof · cited by 0
Set.sups_union_rightproof · cited by 0