Mathlib Map

Theorems · Definition · order theory

Sublocale.carrier

{X : Type u_2} → [inst : Order.Frame X] → Sublocale X → Set X

The set corresponding to the sublocale.

Defined in
Mathlib.Order.Sublocale
Cited by
3 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Order.Frame
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Sublocale.himp_mem' · cited by 1Sublocale.himp_mem'Sublocale.sInf_mem' · cited by 1Sublocale.sInf_mem'Sublocale.mem_carrier · cited by 0Sublocale.mem_carrierSet · cited by 53352SetOrder.Frame · cited by 88Order.FrameSublocale · cited by 30SublocaleSublocale.carrierCITED BYCITES

Cites3

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

  • Setstatement · cited by 53,352
  • Order.Framestatement and proof · cited by 88
  • Sublocalestatement and proof · cited by 30

Cited by3

Results whose statement or proof uses this declaration.