Mathlib Map

Theorems · Definition · order theory

LinOrd.carrier

LinOrd → Type u_2

The underlying linearly ordered type.

Defined in
Mathlib.Order.Defs.LinearOrder
Cited by
48 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LinOrd.Hom.hom · cited by 18Hom.homLinOrd.dual · cited by 5LinOrd.dualNonemptyFinLinOrd.dual · cited by 4NonemptyFinLinOrd.dualNonemptyFinLinOrd.hom_ext · cited by 3NonemptyFinLinOrd.hom_extOrderType.inductionOn · cited by 3OrderType.inductionOnNonemptyFinLinOrd.dualEquiv · cited by 2NonemptyFinLinOrd.dualEqu…LinOrd.dualEquiv · cited by 2LinOrd.dualEquivOrderType.ToType · cited by 2OrderType.ToTypeLinOrd.Hom.ext · cited by 2Hom.extLinOrd.Hom.hom' · cited by 2Hom.hom'OrderType.liftOn · cited by 2OrderType.liftOnLinOrd.Iso.mk · cited by 2Iso.mkOrderType.liftOn₂ · cited by 2OrderType.liftOn₂NonemptyFinLinOrd.Iso.mk · cited by 2Iso.mkNonemptyFinLinOrd.mk.inj · cited by 1mk.injLinOrd · cited by 46LinOrdLinOrd.carrierCITED BYCITES

Cites1

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

  • LinOrdstatement and proof · cited by 46

Cited by70

Results whose statement or proof uses this declaration.