Mathlib Map

Theorems · Definition · logic and foundations

Subtype.map

{α : Sort u_1} →
  {β : Sort u_2} → {p : α → Prop} → {q : β → Prop} → (f : α → β) → (∀ (a : α), p a → q (f a)) → Subtype p → Subtype q

Restriction of a function to a function on subtypes.

Defined in
Mathlib.Data.Subtype
Cited by
52 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.MapsTo.restrict · cited by 57MapsTo.restrictQuasispectrumRestricts.nonUnitalStarAlgHom · cited by 10QuasispectrumRestricts.no…SpectrumRestricts.starAlgHom · cited by 10SpectrumRestricts.starAlg…Unitary.map · cited by 10Unitary.mapStarSubalgebra.inclusion · cited by 9StarSubalgebra.inclusioncfcₙHomSuperset · cited by 7cfcₙHomSupersetSubtype.map_injective · cited by 7Subtype.map_injectiveFinset.prod_add · cited by 7Finset.prod_addcfcHomSuperset · cited by 6cfcHomSupersetSubtype.map_coe · cited by 5Subtype.map_coeQuasispectrumRestricts.nonUnitalStarAlgHom_apply · cited by 4QuasispectrumRestricts.no…SpectrumRestricts.starAlgHom_apply · cited by 4SpectrumRestricts.starAlg…continuousOn_cfc · cited by 4continuousOn_cfcFunction.Embedding.subtypeMap · cited by 4Embedding.subtypeMapContinuous.subtype_map · cited by 3Continuous.subtype_mapSubtype.mapCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by62

Results whose statement or proof uses this declaration.