Mathlib Map

Theorems · Theorem · group theory

Set.image2_add

∀ {α : Type u_2} [inst : Add α] {s t : Set α}, Set.image2 (fun x1 x2 => x1 + x2) s t = s + t
Defined in
Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by
6 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Add
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

QuotientAddGroup.preimage_image_mk_eq_add · cited by 3QuotientAddGroup.preimage…Cardinal.mk_add_le · cited by 2Cardinal.mk_add_leSet.image_op_vadd · cited by 2Set.image_op_vaddLinearMap.coprod_map_prod · cited by 2LinearMap.coprod_map_prodMultiplicative.ofAdd_image_setAdd · cited by 1Multiplicative.ofAdd_imag…Multiplicative.toAdd_image_setMul · cited by 1Multiplicative.toAdd_imag…Set · cited by 53352SetSet.add · cited by 338Set.addSet.image2 · cited by 311Set.image2Set.image2_addCITED BYCITES

Cites3

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.addstatement · cited by 338
  • Set.image2statement · cited by 311

Cited by6

Results whose statement or proof uses this declaration.