Mathlib Map

Theorems · Definition · logic and foundations

PFun.asSubtype

{α : Type u_1} → {β : Type u_2} → (f : α →. β) → ↑f.Dom → β

Turns a partial function into a function out of its domain.

Defined in
Mathlib.Data.PFun
Cited by
2 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PFun.preimage_asSubtype · cited by 0PFun.preimage_asSubtypePFun.equivSubtype · cited by 0PFun.equivSubtypePFun.asSubtype_eq_of_mem · cited by 0PFun.asSubtype_eq_of_memSet.Elem · cited by 7166Set.ElemPFun · cited by 207PFunPFun.Dom · cited by 28PFun.DomPFun.fn · cited by 6PFun.fnPFun.asSubtypeCITED BYCITES

Cites4

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

  • Set.Elemstatement and proof · cited by 7,166
  • PFunstatement and proof · cited by 207
  • PFun.Domstatement and proof · cited by 28
  • PFun.fnproof · cited by 6

Cited by3

Results whose statement or proof uses this declaration.