Theorems · Definition · order theory
Sublocale.toNucleus
{X : Type u_1} → [inst : Order.Frame X] → Sublocale X → Nucleus XThe restriction from the locale X into a sublocale is a nucleus.
- Defined in
- Mathlib.Order.Sublocale
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Order.Frame
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Order.Framestatement and proof · cited by 88
- Nucleusstatement · cited by 41
- Sublocalestatement and proof · cited by 30
- Sublocale.restrictproof · cited by 4
Cited by5
Results whose statement or proof uses this declaration.
- nucleusIsoSublocaleproof · cited by 2
- Sublocale.range_toNucleusstatement · cited by 1
- Sublocale.toNucleus_applystatement and proof · cited by 1
- Sublocale.toNucleus_le_toNucleusstatement · cited by 0
- nucleusIsoSublocale.symm_eq_toNucleusstatement · cited by 0