gaugeRescale_self_apply
theorem gaugeRescale_self_apply :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : T1Space E]
{s : Set E}, Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → ∀ (x : E), gaugeRescale s s x = x
This theorem states that, for any type `E` that forms an additive commutative group and a module over the real numbers, and additionally has a topological space structure and a T1 space structure (meaning that for any two distinct points, there is an open set containing one but not the other), if we have a set `s` of type `E` that is absorbent and Von Neumann bounded, then for any element `x` of type `E`, the gauge rescale of `s` with respect to itself at `x` is just `x`. In other words, gauge rescale doesn't change the points of the set `s` provided `s` is absorbent and Von Neumann bounded. This can be thought as a kind of normalization property for absorbent and Von Neumann bounded sets in such a structured space.
More concisely: Given a type `E` that forms an additive commutative group and a module over the real numbers, is a T1 topological space, and contains an absorbent and Von Neumann bounded set `s`, for all `x` in `E`, the gauge rescale of `s` with respect to itself at `x` equals `x`.
|
gaugeRescale_zero
theorem gaugeRescale_zero :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E), gaugeRescale s t 0 = 0
The theorem `gaugeRescale_zero` states that for any given type `E` which is an additive commutative group and also a real number module, and for any two sets `s` and `t` of type `E`, the gauge rescale of 0 with respect to these sets is also 0. In other words, when you apply the function `gaugeRescale` with the sets `s` and `t` to the element 0 in `E`, the result is always 0. This function `gaugeRescale` is defined to map each point `x` to a point `y` on the same ray that has the same gauge (a measure of size in a certain sense) with respect to `t` as `x` has with respect to `s`.
More concisely: For any additive commutative group `E` that is a real number module, and for any sets `s` and `t` of elements in `E`, the gauge rescale of 0 with respect to `s` and `t` is equal to 0.
|