Mathlib Map

Theorems · Definition · order theory

LowerSet.carrier

{α : Type u_1} → [inst : LE α] → LowerSet α → Set α

The carrier of a LowerSet.

Defined in
Mathlib.Order.Defs.Unbundled
Cited by
11 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LowerSet.lower' · cited by 3LowerSet.lower'Order.Ideal.nonempty' · cited by 2Ideal.nonempty'Order.Ideal.casesOn · cited by 1Ideal.casesOnOrder.Ideal.mk.inj · cited by 1mk.injOrder.Ideal.mk.noConfusion · cited by 1mk.noConfusionOrder.Ideal.directed' · cited by 1Ideal.directed'Order.Ideal.toLowerSet_injective · cited by 1Ideal.toLowerSet_injectiveOrder.Ideal.noConfusion · cited by 0Ideal.noConfusionOrder.Ideal.noConfusionType · cited by 0Ideal.noConfusionTypeOrder.Ideal.carrier_eq_coe · cited by 0Ideal.carrier_eq_coeOrder.Ideal.recOn · cited by 0Ideal.recOnLowerSet.carrier_eq_coe · cited by 0LowerSet.carrier_eq_coeOrder.Ideal.mk.congr_simp · cited by 0mk.congr_simpOrder.Ideal.mk.injEq · cited by 0mk.injEqOrder.Ideal.mk.sizeOf_spec · cited by 0mk.sizeOf_specSet · cited by 53352SetLowerSet · cited by 230LowerSetLowerSet.carrierCITED BYCITES

Cites2

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

  • Setstatement · cited by 53,352
  • LowerSetstatement and proof · cited by 230

Cited by16

Results whose statement or proof uses this declaration.