Mathlib Map

Theorems · Definition · logic and foundations

PFun.Dom

{α : Type u_1} → {β : Type u_2} → (α →. β) → Set α

The domain of a partial function

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

Around this declaration

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

PFun.fn · cited by 6PFun.fnPFun.restrict · cited by 2PFun.restrictPFun.asSubtype · cited by 2PFun.asSubtypePFun.mem_dom · cited by 2PFun.mem_domPFun.preimage_eq · cited by 2PFun.preimage_eqDioph.diophFn_comp1 · cited by 1Dioph.diophFn_comp1Dioph.diophPFun_comp1 · cited by 1Dioph.diophPFun_comp1PFun.compl_dom_subset_core · cited by 1PFun.compl_dom_subset_corePFun.dom_iff_graph · cited by 1PFun.dom_iff_graphPFun.preimage_subset_dom · cited by 1PFun.preimage_subset_domPFun.preimage_univ · cited by 1PFun.preimage_univPFun.pure_defined · cited by 0PFun.pure_definedopen_dom_of_pcontinuous · cited by 0open_dom_of_pcontinuousPFun.fn.congr_simp · cited by 0fn.congr_simpPFun.restrict.congr_simp · cited by 0restrict.congr_simpSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredPFun · cited by 207PFunPart.Dom · cited by 145Part.DomPFun.DomCITED BYCITES

Cites4

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

  • Setstatement · cited by 53,352
  • Set.ofPredproof · cited by 6,101
  • PFunstatement and proof · cited by 207
  • Part.Domproof · cited by 145

Cited by32

Results whose statement or proof uses this declaration.