Filter.Tendsto.abs
theorem Filter.Tendsto.abs :
∀ {α : Type u_1} {G : Type u_2} [inst : TopologicalSpace G] [inst_1 : LinearOrderedAddCommGroup G]
[inst_2 : OrderTopology G] {l : Filter α} {f : α → G} {a : G},
Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => |f x|) l (nhds |a|)
The theorem `Filter.Tendsto.abs` states that for any types `α` and `G`, where `G` is equipped with a topological space structure, a linear ordered additive commutative group structure, and an order topology, given a filter `l` on `α`, a function `f` from `α` to `G`, and a point `a` in `G`, if `f` tends to `a` along `l` (i.e., for every neighborhood of `a` in `G`, the preimage under `f` of that neighborhood is a neighborhood in `l`), then the absolute value function applied to `f`, i.e., `|f(x)|`, also tends to `|a|` along `l`. In other words, this theorem asserts that the limit of the absolute value of a function is the absolute value of the limit of the function, under the conditions described.
More concisely: If a filter on a space converges to a point in a topological group under a function, then the absolute value of the function converges to the absolute value of the point under the filter.
|
continuous_abs
theorem continuous_abs :
∀ {G : Type u_2} [inst : TopologicalSpace G] [inst_1 : LinearOrderedAddCommGroup G] [inst_2 : OrderTopology G],
Continuous abs
The theorem `continuous_abs` states that for any type `G` which is a topological space, a linearly ordered additive commutative group, and has an order topology, the function `abs` is continuous. In mathematical terms, this is expressing the fact that the absolute value function is continuous over any linearly ordered additive commutative group that is furnished with an order topology.
More concisely: The absolute value function is continuous on any linearly ordered additive commutative group endowed with an order topology.
|