Theorems · Definition · logic and foundations
PFun.preimage
{α : Type u_1} → {β : Type u_2} → (α →. β) → Set β → Set αPreimage of a set under a partial function.
- Defined in
- Mathlib.Data.PFun
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- PFunstatement and proof · cited by 207
- SetRel.preimageproof · cited by 56
- PFun.graph'proof · cited by 11
Cited by19
Results whose statement or proof uses this declaration.
- Filter.ptendsto'_defstatement · cited by 3
- PContinuousproof · cited by 2
- PFun.preimage_eqstatement and proof · cited by 2
- PFun.preimage_subset_corestatement and proof · cited by 2
- PFun.preimage_monostatement · cited by 1
- PFun.preimage_subset_domstatement and proof · cited by 1
- PFun.preimage_univstatement · cited by 1
- pcontinuous_iff'proof · cited by 0
- ptendsto'_nhdsstatement · cited by 0
- PFun.preimage_unionstatement · cited by 0
- PFun.Preimage_defstatement · cited by 0
- PFun.mem_preimagestatement · cited by 0