Mathlib Map

Theorems · Theorem · functional analysis

lipschitzWith_posPart

∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  LipschitzWith 1 posPart
Defined in
Mathlib.Analysis.Normed.Order.Lattice
Cited by
2 results in Mathlib
Foundations
Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroupLatticeHasSolidNormIsOrderedAddMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

continuous_posPart · cited by 12continuous_posPartlipschitzWith_negPart · cited by 1lipschitzWith_negPartNormedAddCommGroup · cited by 15752NormedAddCommGroupNNReal · cited by 4310NNRealIsOrderedAddMonoid · cited by 1659IsOrderedAddMonoidLattice · cited by 916LatticeLipschitzWith · cited by 316LipschitzWithPosPart.posPart · cited by 113PosPart.posPartHasSolidNorm · cited by 67HasSolidNormlipschitzWith_sup_right · cited by 1lipschitzWith_sup_rightlipschitzWith_posPartCITED BYCITES

Cites8

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

Cited by2

Results whose statement or proof uses this declaration.