Mathlib Map

Theorems · Theorem · order theory

Set.mapsTo_id

∀ {α : Type u_1} (s : Set α), Set.MapsTo id s s
Defined in
Mathlib.Data.Set.Function
Cited by
8 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_id · cited by 3Set.bijOn_idContMDiffWithinAt.mfderivWithin_const · cited by 3ContMDiffWithinAt.mfderiv…LipschitzOnWith.locallyBoundedVariationOn · cited by 3LipschitzOnWith.locallyBo…Flow.isInvariant_omegaLimit · cited by 1Flow.isInvariant_omegaLim…SimpleGraph.induceHom_id · cited by 1SimpleGraph.induceHom_idSubmodule.inf_iSup_genEigenspace · cited by 1Submodule.inf_iSup_genEig…Bundle.Trivialization.contMDiffOn · cited by 1Trivialization.contMDiffOnSimpleGraph.induceHomOfLE_toHom · cited by 0SimpleGraph.induceHomOfLE…Set · cited by 53352SetSet.MapsTo · cited by 732Set.MapsToSet.mapsTo_idCITED 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 by8

Results whose statement or proof uses this declaration.