Mathlib Map

Theorems · Theorem · order theory

Set.mapsTo_empty

∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β), Set.MapsTo f ∅ t
Defined in
Mathlib.Data.Set.Function
Cited by
4 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.bijOn_empty · cited by 5Set.bijOn_emptyisMulFreimanHom_empty · cited by 0isMulFreimanHom_emptyFilter.HasBasis.nhds_continuousMapConst · cited by 0HasBasis.nhds_continuousM…isAddFreimanHom_empty · cited by 0isAddFreimanHom_emptySet · cited by 53352SetSet.MapsTo · cited by 732Set.MapsToSet.mapsTo_emptyCITED BYCITES

Cites2

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 · cited by 732

Cited by4

Results whose statement or proof uses this declaration.