Mathlib Map

Theorems · Theorem · order theory

Set.mapsTo_univ

∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.MapsTo f s Set.univ
Defined in
Mathlib.Data.Set.Function
Cited by
55 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.

Continuous.comp_continuousOn · cited by 52Continuous.comp_continuou…ContDiffAt.comp · cited by 34ContDiffAt.compHasFDerivAt.comp_hasFDerivWithinAt · cited by 31HasFDerivAt.comp_hasFDeri…ContDiffAt.comp_contDiffWithinAt · cited by 28ContDiffAt.comp_contDiffW…ContinuousAt.comp_continuousWithinAt · cited by 25ContinuousAt.comp_continu…HasDerivAt.comp_hasDerivWithinAt · cited by 21HasDerivAt.comp_hasDerivW…ContDiff.comp_contDiffOn · cited by 20ContDiff.comp_contDiffOnContDiffWithinAt.comp · cited by 18ContDiffWithinAt.compContDiffWithinAt.prodMk · cited by 17ContDiffWithinAt.prodMkContMDiffAt.comp · cited by 16ContMDiffAt.compDifferentiableAt.comp_differentiableWithinAt · cited by 14DifferentiableAt.comp_dif…ContMDiffAt.comp_contMDiffWithinAt · cited by 14ContMDiffAt.comp_contMDif…AnalyticAt.comp_analyticWithinAt · cited by 10AnalyticAt.comp_analyticW…HasFDerivAt.comp_hasDerivWithinAt · cited by 7HasFDerivAt.comp_hasDeriv…ContDiffWithinAt.continuousLinearMap_comp · cited by 6ContDiffWithinAt.continuo…Set · cited by 53352SetSet.univ · cited by 3945Set.univSet.MapsTo · cited by 732Set.MapsToSet.mapsTo_univCITED 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.univstatement · cited by 3,945
  • Set.MapsTostatement · cited by 732

Cited by55

Results whose statement or proof uses this declaration.