Theorems · Theorem · group theory

Set.MapsTo.add

∀ {α : Type u_2} {β : Type u_3} [inst : Add β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ A B₁ → Set.MapsTo f₂ A B₂ → Set.MapsTo (f₁ + f₂) A (B₁ + B₂)

Defined in: Mathlib.Algebra.Group.Pointwise.Set.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: Add

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.MapsTostatement and proof · cited by 732
Set.addstatement · cited by 338
Set.add_mem_addproof · cited by 30

Cited by1

Results whose statement or proof uses this declaration.

IsAddFreimanHom.addproof · cited by 0