Theorems · Theorem · order theory

Set.image2_inter_union_subset_union

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

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

Cites9

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
le_reflproof · cited by 2,061
le_imp_le_of_le_of_leproof · cited by 576
Set.inter_subset_leftproof · cited by 360
Set.inter_subset_rightproof · cited by 329
Set.image2statement and proof · cited by 311
Set.union_subset_unionproof · cited by 29
Set.image2_subsetproof · cited by 25
Set.image2_union_rightproof · cited by 13

Cited by10

Results whose statement or proof uses this declaration.

Finset.image₂_inter_union_subset_unionproof · cited by 6
Set.image2_inter_union_subsetproof · cited by 4
Set.inter_vadd_union_subset_unionproof · cited by 0
Set.inter_sdiv_union_subset_unionproof · cited by 0
Set.inter_vsub_union_subset_unionproof · cited by 0
Set.inter_add_union_subset_unionproof · cited by 0
Set.inter_smul_union_subset_unionproof · cited by 0
Set.inter_sub_union_subset_unionproof · cited by 0
Set.inter_mul_union_subset_unionproof · cited by 0
Set.inter_div_union_subset_unionproof · cited by 0