lipschitzWith_posPart
theorem lipschitzWith_posPart : ∀ {α : Type u_1} [inst : NormedLatticeAddCommGroup α], LipschitzWith 1 posPart := by
sorry
This theorem states that for any normed lattice-ordered additive commutative group `α`, the function `posPart`, which gives the positive part of an element in `α`, is Lipschitz continuous with constant `1`. In mathematical terms, this means that for any two elements `x` and `y` in the group, the distance (in the sense of the pseudo-metric on the group) between their positive parts is less than or equal to the distance between `x` and `y` itself.
More concisely: For any normed lattice-ordered additive commutative group `α`, the function `posPart` is Lipschitz continuous with constant `1`, i.e., `||posPart x - posPart y|| ≤ ||x - y||` for all `x, y` in `α`.
|
LatticeOrderedAddCommGroup.isSolid_ball
theorem LatticeOrderedAddCommGroup.isSolid_ball :
∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [inst_2 : HasSolidNorm α] (r : ℝ),
LatticeOrderedAddCommGroup.IsSolid (Metric.ball 0 r)
This theorem states that if a type `α` has a solid norm, then the balls centered at the origin in `α` are solid sets. More specifically, a solid set in a lattice ordered group is one where for any element `x` in the set, and any other element `y` in `α`, if the absolute value of `y` is less than or equal to the absolute value of `x`, then `y` is also in the set. In this context, a ball centered at the origin is the set of all points `y` with a distance from the origin less than a real number `r`. Therefore, the theorem asserts that such a ball is a solid set under the given conditions.
More concisely: If a type `α` has a solid norm, then the balls centered at the origin in `α` are solid sets. That is, for all `x` in the ball and `y` in `α` with `|y| ≤ |x|`, `y` is in the ball.
|