Theorems · Theorem · order theory
Nucleus.le_apply
∀ {X : Type u_1} [inst : SemilatticeInf X] {n : Nucleus X} {x : X}, x ≤ n x- Defined in
- Mathlib.Order.Nucleus
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemilatticeInf
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.coestatement · cited by 62,936
- SemilatticeInfstatement and proof · cited by 634
- Nucleusstatement and proof · cited by 41
- ClosureOperator.le_closureproof · cited by 19
- Nucleus.toClosureOperatorproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- Nucleus.map_himp_leproof · cited by 1
- Nucleus.comp_eq_right_iff_leproof · cited by 1
- Nucleus.restrict_toSublocaleproof · cited by 0
- Nucleus.map_himp_applyproof · cited by 0
- Nucleus.range_subset_rangeproof · cited by 0