Mathlib Map

Theorems · Definition · order theory

LTSeries.mk

{α : Type u_1} → [inst : Preorder α] → (length : ℕ) → (toFun : Fin (length + 1) → α) → StrictMono toFun → LTSeries α

An alternative constructor of LTSeries from a strictly monotone function.

Defined in
Mathlib.Order.RelSeries
Cited by
3 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LTSeries.map · cited by 15LTSeries.mapLTSeries.comap · cited by 3LTSeries.comapOrder.height_eq_krullDim_Iic · cited by 2Order.height_eq_krullDim_…LTSeries.injStrictMono · cited by 0LTSeries.injStrictMonoLTSeries.mk_length · cited by 0LTSeries.mk_lengthLTSeries.mk_toFun · cited by 0LTSeries.mk_toFunPreorder · cited by 7952PreorderStrictMono · cited by 706StrictMonoLTSeries · cited by 87LTSeriesLTSeries.mkCITED BYCITES

Cites3

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

Cited by6

Results whose statement or proof uses this declaration.