Mathlib Map

Theorems · Definition · order theory

Set.projIcc

{α : Type u_1} → [inst : LinearOrder α] → (a b : α) → a ≤ b → α → ↑(Set.Icc a b)

Projection of α to the closed interval [a, b].

Defined in
Mathlib.Order.Interval.Set.ProjIcc
Cited by
56 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext
Assumes
LinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.IccExtend · cited by 26Set.IccExtendSet.projIcc_val · cited by 14Set.projIcc_valODE.FunSpace.compProj · cited by 13FunSpace.compProjSet.projIcc_of_mem · cited by 11Set.projIcc_of_memcontinuous_projIcc · cited by 9continuous_projIccGenLoop.transAt · cited by 6GenLoop.transAtunitInterval.qRight · cited by 6unitInterval.qRightSet.Icc.addNSMul · cited by 6Icc.addNSMulMetric.PiNatEmbed.distDenseSeq · cited by 6PiNatEmbed.distDenseSeqSet.projIcc_of_le_left · cited by 5Set.projIcc_of_le_leftSet.projIcc_of_right_le · cited by 5Set.projIcc_of_right_leSet.monotone_projIcc · cited by 4Set.monotone_projIcccontMDiffOn_projIcc · cited by 4contMDiffOn_projIccManifold.riemannianEDist_le_pathELength · cited by 4Manifold.riemannianEDist_…ODE.FunSpace.compProj_apply · cited by 3FunSpace.compProj_applyLinearOrder · cited by 8572LinearOrderSet.Elem · cited by 7166Set.ElemSet.Icc · cited by 1702Set.IccSet.projIccCITED BYCITES

Cites3

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

Cited by63

Results whose statement or proof uses this declaration.