Theorems · Definition · order theory
SetRel.core
{α : Type u_1} → {β : Type u_2} → SetRel α β → Set β → Set αCore of a set S : Set β w.R.t R : SetRel α β is the set of x : α that are related only
to elements of S. Other generalization of Function.preimage.
- Defined in
- Mathlib.Data.Rel
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.ofPredproof · cited by 6,101
- SetRelstatement and proof · cited by 581
Cited by22
Results whose statement or proof uses this declaration.
- PFun.coreproof · cited by 16
- Filter.rmapproof · cited by 5
- Filter.rcomapproof · cited by 4
- SetRel.core_monostatement · cited by 3
- SetRel.core_compstatement · cited by 2
- SetRel.image_subset_iffstatement · cited by 1
- Filter.rcomap_rcomapproof · cited by 1
- SetRel.core_interstatement and proof · cited by 1
- Filter.rtendsto_defstatement · cited by 1
- SetRel.core_subset_corestatement and proof · cited by 1
- Filter.rmap_rmapproof · cited by 1
- rtendsto_nhdsstatement · cited by 1