uniqueDiffWithinAt_convex
theorem uniqueDiffWithinAt_convex :
ā {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ā G] {s : Set G},
Convex ā s ā (interior s).Nonempty ā ā {x : G}, x ā closure s ā UniqueDiffWithinAt ā s x
This theorem states that in a real vector space, if a set is convex and its interior is nonempty, then any point in the closure of this set is a point of unique differentiability within the set. In other words, for such a set in a normed addative commutative group that also forms a normed space over the real numbers, every point in the closure of the set has a unique tangent space and a unique derivative, if the derivative exists, within the set. This property of unique differentiability is captured by the mathematical concept of 'UniqueDiffWithinAt'.
More concisely: In a real normed additive commutative group, if a convex set with nonempty interior has a point in its closure, then every point in the closure is uniquely differentiable within the set.
|
uniqueDiffOn_convex
theorem uniqueDiffOn_convex :
ā {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ā G] {s : Set G},
Convex ā s ā (interior s).Nonempty ā UniqueDiffOn ā s
The theorem `uniqueDiffOn_convex` states that in a real normed additive commutative group (which is also a normed space over the real numbers), any convex set with a non-empty interior is uniquely differentiable. This means that for any such set, each point in the set has a unique tangent space, or equivalently, a unique derivative for every differentiable function defined on the set.
More concisely: In a real normed additive commutative group with a non-empty interior, every convex set is uniquely differentiable.
|
UniqueDiffOn.pi
theorem UniqueDiffOn.pi :
ā {š : Type u_1} [inst : NontriviallyNormedField š] (Ī¹ : Type u_5) [inst_1 : Finite Ī¹] (E : Ī¹ ā Type u_6)
[inst_2 : (i : Ī¹) ā NormedAddCommGroup (E i)] [inst_3 : (i : Ī¹) ā NormedSpace š (E i)] (s : (i : Ī¹) ā Set (E i))
(I : Set Ī¹), (ā i ā I, UniqueDiffOn š (s i)) ā UniqueDiffOn š (I.pi s)
This theorem, named `UniqueDiffOn.pi`, states that the finite product of a family of sets, where each set satisfies the property of unique differentiability, is also a set which satisfies the property of unique differentiability. Here, the family of sets is indexed by a finite set `I`. The product is taken over a field `š`, which is assumed to be nontrivially normed. Each set in the family is a subset of a normed additive commutative group, which is in turn a normed space over the field `š`. The theorem asserts that, if each set in the family is uniquely differentiable, then the product set (constructed via the `pi` function) is also uniquely differentiable.
More concisely: If each set in a finite family, indexed by a field, of uniquely differentiable subsets of normed additive commutative groups over a nontrivially normed field is itself a subset of a normed space, then their finite product is also a uniquely differentiable subset of the product normed space.
|
UniqueDiffWithinAt.mono_nhds
theorem UniqueDiffWithinAt.mono_nhds :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E} {s t : Set E},
UniqueDiffWithinAt š s x ā nhdsWithin x s ā¤ nhdsWithin x t ā UniqueDiffWithinAt š t x
This theorem states that for any non-trivially normed field `š` and a normed additively commutative group `E`, which is also a normed space over `š`, if there exists a unique tangent differential at a point `x` within a set `s` and the neighborhood within `s` at `x` is a subset of the neighborhood within another set `t` at `x`, then there also exists a unique tangent differential at `x` within the set `t`. In other words, if we can uniquely differentiate within a certain 'neighbourhood' (defined by set `s`) of `x`, and that neighbourhood is included within a larger neighbourhood defined by set `t`, then we can also uniquely differentiate within the larger neighbourhood.
More concisely: If a normed space `E` over a non-trivially normed field `š`, with unique tangent differentials at a point `x` in sets `s` and `t` (where `s` is a subset of `t`), then the tangent differential at `x` in `E` with respect to `š` is unique.
|
mem_tangentCone_of_openSegment_subset
theorem mem_tangentCone_of_openSegment_subset :
ā {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ā G] {s : Set G} {x y : G},
openSegment ā x y ā s ā y - x ā tangentConeAt ā s x
The theorem `mem_tangentCone_of_openSegment_subset` states that for any subset `s` of a real vector space, if this subset contains an open segment from `x` to `y`, then the direction of this segment, given by `y - x`, belongs to the tangent cone to the subset `s` at the point `x`. This theorem is applicable in the context of a normed additive commutative group with a normed space structure over the real numbers.
More concisely: If a subset of a real normed vector space contains an open segment between points `x` and `y`, then the direction vector `y - x` is in the tangent cone of `s` at `x`.
|
uniqueDiffOn_Ici
theorem uniqueDiffOn_Ici : ā (a : ā), UniqueDiffOn ā (Set.Ici a)
The theorem `uniqueDiffOn_Ici` states that for every real number `a`, the left-closed right-infinite interval `[a, ā)` is a uniquely differentiable set. This means that each point in the interval has a unique derivative (or equivalently, the derivative function is uniquely defined at each point). Here, `Set.Ici a` represents the interval `[a, ā)` and `UniqueDiffOn ā (Set.Ici a)` expresses the unique differentiability of this interval in the field of real numbers.
More concisely: For every real number `a`, the function `x ā¦ d/dx (f x)` has a unique value for all `x ā [a, ā)`, where `f` is the derivative function.
|
tangentCone_congr
theorem tangentCone_congr :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E} {s t : Set E},
nhdsWithin x s = nhdsWithin x t ā tangentConeAt š s x = tangentConeAt š t x
This theorem states that the tangent cone of a set `s` at a point `x` depends only on the neighborhood of `x` within `s`. More formally, for a given NontriviallyNormedField `š` and a NormedSpace `E` over `š`, and given two sets `s` and `t` of `E`, if the neighborhood of `x` within `s` is the same as the neighborhood of `x` within `t`, then the tangent cone of `s` at `x` is the same as the tangent cone of `t` at `x`.
More concisely: If two sets in a NormedSpace over a NontriviallyNormedField have the same neighborhood at a point, then they have equal tangent cones at that point.
|
subset_tangentCone_prod_left
theorem subset_tangentCone_prod_left :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {x : E}
{s : Set E} {t : Set F} {y : F},
y ā closure t ā ā(LinearMap.inl š E F) '' tangentConeAt š s x ā tangentConeAt š (s ĆĖ¢ t) (x, y)
The theorem `subset_tangentCone_prod_left` states that for any non-trivially normed field `š`, normed additive commutative group `E` and `F`, any point `x` in `E`, sets `s` and `t` in `E` and `F` respectively, and any point `y` in `F` that belongs to the closure of `t`, the image of the tangent cone at `s` at point `x` under the left injection linear map is a subset of the tangent cone at the product of `s` and `t` at the point `(x, y)`. In simpler words, it states that in a product space, the tangent cone at a point of the product contains the tangent cone of the left factor at the corresponding point.
More concisely: For any non-trivially normed field š, normed additive commutative groups E and F, and points x in E, s in E, t in F with y in the closure of t, the image of the tangent cone of s at x under the left injection linear map is contained in the tangent cone of the product sĆt at (x,y).
|
UniqueDiffOn.prod
theorem UniqueDiffOn.prod :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {s : Set E}
{t : Set F}, UniqueDiffOn š s ā UniqueDiffOn š t ā UniqueDiffOn š (s ĆĖ¢ t)
The theorem "UniqueDiffOn.prod" states that for any non-trivially normed field `š`, and any two normed additive commutative groups `E` and `F` over `š`, if `s` is a set of unique differentiability in `E` and `t` is a set of unique differentiability in `F`, then the Cartesian product of `s` and `t` (denoted as `s ĆĖ¢ t`) forms a set of unique differentiability over `š`. In other words, if each element in the sets `s` and `t` can be differentiated uniquely, then any pair in the Cartesian product of `s` and `t` can also be differentiated uniquely.
More concisely: Given any non-trivially normed field `š` and normed additive commutative groups `E` and `F` over `š` with sets `s` of unique differentiability in `E` and `t` of unique differentiability in `F`, the Cartesian product `s ĆĖ¢ t` forms a set of unique differentiability over `š`.
|
UniqueDiffOn.univ_pi
theorem UniqueDiffOn.univ_pi :
ā {š : Type u_1} [inst : NontriviallyNormedField š] (Ī¹ : Type u_5) [inst_1 : Finite Ī¹] (E : Ī¹ ā Type u_6)
[inst_2 : (i : Ī¹) ā NormedAddCommGroup (E i)] [inst_3 : (i : Ī¹) ā NormedSpace š (E i)] (s : (i : Ī¹) ā Set (E i)),
(ā (i : Ī¹), UniqueDiffOn š (s i)) ā UniqueDiffOn š (Set.univ.pi s)
This theorem states that the finite product of a family of sets that each have unique differentiability properties also has unique differentiability properties. Here, "unique differentiability" is a property of a set in a normed field, implying that every point in the set has a unique differential. The theorem's assumptions include that each set in the family is of unique differentiability, the family is indexed by a finite type, and each set is in a normed additive commutative group that is a normed space over a non-trivially normed field. The theorem concludes that the product set, formed by taking all possible combinations of elements from the individual sets in the family, also has unique differentiability properties.
More concisely: Given a family of sets in a normed additive commutative group over a non-trivially normed field, each of which has unique differentiability properties, the finite product of these sets also has unique differentiability properties.
|
IsOpen.uniqueDiffOn
theorem IsOpen.uniqueDiffOn :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {s : Set E}, IsOpen s ā UniqueDiffOn š s
This theorem states that for any nontrivially normed field `š` and any normed add commutative group `E` that is also a normed space over `š`, if `s` is an open set in `E`, then `s` is uniquely differentiable with respect to `š`. In simpler terms, it says that any open set in a normed space is uniquely differentiable.
More concisely: For any nontrivially normed field `š` and normed additive group `E` that is also a normed space over `š`, every open set in `E` is uniquely differentiable as a function from `š` to `E`.
|
Mathlib.Analysis.Calculus.TangentCone._auxLemma.11
theorem Mathlib.Analysis.Calculus.TangentCone._auxLemma.11 :
ā {Ī± : Type u_1} [inst : Preorder Ī±] {a b : Ī±} [inst_1 : DenselyOrdered Ī±], (Set.Ioo a b).Nonempty = (a < b) := by
sorry
This theorem states that for any type `Ī±` with a `Preorder` relation, and any two elements `a` and `b` of this type such that `Ī±` is `DenselyOrdered`, the left-open right-open interval `(a, b)` is nonempty if and only if `a` is less than `b`. In other words, there exists at least one element `x` that strictly lies between `a` and `b` (`a < x < b`) if and only if `a < b`.
More concisely: For any densely ordered type `Ī±` with a `Preorder` relation, the interval `(a, b)` is nonempty if and only if `a` is strictly less than `b`.
|
uniqueDiffOn_Icc_zero_one
theorem uniqueDiffOn_Icc_zero_one : UniqueDiffOn ā (Set.Icc 0 1)
The theorem `uniqueDiffOn_Icc_zero_one` states that the real interval `[0, 1]`, which is the set of real numbers `x` where `0 ā¤ x` and `x ā¤ 1`, is a set of unique differentiability. This means that for each point in this interval, there exists a unique derivative (rate of change of a function) at that point.
More concisely: The real interval [0, 1] is an interval of uniqueness for real-valued differentiability.
|
tangentCone_inter_nhds
theorem tangentCone_inter_nhds :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E} {s t : Set E}, t ā nhds x ā tangentConeAt š (s ā© t) x = tangentConeAt š s x
This theorem, called `tangentCone_inter_nhds`, states that for any nontrivially normed field `š`, normed additive commutative group `E`, and a point `x` in `E`, given two sets `s` and `t` of `E` where `t` is a neighborhood of `x`, the tangent cone at the point `x` of the intersection of `s` and `t` is the same as the tangent cone at `x` of `s`. Simply put, intersecting a set with a neighborhood of a point does not change the set's tangent cone at that point.
More concisely: The tangent cone of a set at a point in a normed additive commutative group is invariant under taking intersections with neighborhoods of that point.
|
uniqueDiffOn_univ
theorem uniqueDiffOn_univ :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E], UniqueDiffOn š Set.univ
The theorem `uniqueDiffOn_univ` states that for any nontrivially normed field `š` and any normed additive commutative group `E` that is also a normed space over `š`, the entire set `Set.univ` (i.e., the set of all elements of `E`) has the property of unique differentiability. In other words, every point in this set has a unique differential, a central concept in differential calculus, when the underlying field is `š` and the space is `E`.
More concisely: For any nontrivially normed field `š` and normed additive commutative group `E` that is also a normed space over `š`, every element in `E` has a unique differential.
|
uniqueDiffWithinAt_congr
theorem uniqueDiffWithinAt_congr :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E} {s t : Set E},
nhdsWithin x s = nhdsWithin x t ā (UniqueDiffWithinAt š s x ā UniqueDiffWithinAt š t x)
The theorem `uniqueDiffWithinAt_congr` states that for any non-trivially normed field `š` and any normed additive commutative group `E` that is a normed space over `š`, given any element `x` of `E` and any two sets `s` and `t` of `E`, if the "neighborhood within" filter of `x` with respect to `s` equals the "neighborhood within" filter of `x` with respect to `t`, then `x` has unique derivatives within `s` if and only if `x` has unique derivatives within `t`. In other words, the property of having unique derivatives at a point within a set is preserved under equivalence of the "neighborhood within" filters.
More concisely: If for all non-trivially normed fields `š` and normed additive commutative groups `E` over `š`, the "neighborhood within" filters of an element `x` in `E` with respect to sets `s` and `t` are equal, then `x` has unique derivatives within `s` if and only if `x` has unique derivatives within `t`.
|
IsOpen.uniqueDiffWithinAt
theorem IsOpen.uniqueDiffWithinAt :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E} {s : Set E}, IsOpen s ā x ā s ā UniqueDiffWithinAt š s x
The theorem `IsOpen.uniqueDiffWithinAt` states that for any nontrivially normed field `š`, any normed additively commutative group `E` that is also a normed space over `š`, any element `x` of `E`, and any set `s` of `E` that is open in the topological space of `E`, if `x` is an element of `s`, then `s` is uniquely differentiable at `x`. In other words, it asserts the uniqueness of differentiation within an open set in a normed space at a particular point that belongs to the set.
More concisely: In a normed space over a nontrivially normed field, if an element is differentiable and belongs to an open set, then the set is uniquely differentiable at that element.
|
UniqueDiffWithinAt.prod
theorem UniqueDiffWithinAt.prod :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {x : E}
{s : Set E} {t : Set F} {y : F},
UniqueDiffWithinAt š s x ā UniqueDiffWithinAt š t y ā UniqueDiffWithinAt š (s ĆĖ¢ t) (x, y)
This theorem states that if we have two sets with unique differentiability at points `x` and `y`, then the product of these two sets also has unique differentiability at the point `(x, y)`. Here, unique differentiability refers to the property where every tangent direction at a point in a set is uniquely determined by the derivative. The sets, labeled `s` and `t`, are of types `E` and `F` respectively. The types `E` and `F` are normed additive commutative groups and also normed spaces over a nontrivial normed field `š`. The points `x` and `y` are elements of `E` and `F` respectively.
More concisely: If sets `s` of type `E` and `t` of type `F`, both having unique differentiability at points `x` in `E` and `y` in `F` respectively, then their product `s Ć t` has unique differentiability at point `(x, y)`.
|
subset_tangentCone_prod_right
theorem subset_tangentCone_prod_right :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {x : E}
{s : Set E} {t : Set F} {y : F},
x ā closure s ā ā(LinearMap.inr š E F) '' tangentConeAt š t y ā tangentConeAt š (s ĆĖ¢ t) (x, y)
This theorem states that for any non-trivially normed field `š`, normed add commutative groups `E` and `F`, and any sets `s` of `E` and `t` of `F`, and any elements `x` of `E` and `y` of `F`, if `x` is in the closure of `s`, then the image of the tangent cone at `y` in `t` under the right injection linear map is a subset of the tangent cone at `(x, y)` in the product set `s ĆĖ¢ t`. In simpler terms, this theorem is about how the tangent cones of Cartesian product sets relate to the tangent cones of their factor sets.
More concisely: For any non-trivially normed field `š`, if `x` is in the closure of a set `s` in a normed additive group `E`, then the image of the tangent cone of a set `t` in a normed additive group `F` under the right injection linear map is a subset of the tangent cone of the product set `s ĆĖ¢ t` at `(x, y)` in `E Ć F`.
|
mapsTo_tangentCone_pi
theorem mapsTo_tangentCone_pi :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {Ī¹ : Type u_5} [inst_1 : DecidableEq Ī¹] {E : Ī¹ ā Type u_6}
[inst_2 : (i : Ī¹) ā NormedAddCommGroup (E i)] [inst_3 : (i : Ī¹) ā NormedSpace š (E i)] {s : (i : Ī¹) ā Set (E i)}
{x : (i : Ī¹) ā E i} {i : Ī¹},
(ā (j : Ī¹), j ā i ā x j ā closure (s j)) ā
Set.MapsTo (ā(LinearMap.single i)) (tangentConeAt š (s i) (x i)) (tangentConeAt š (Set.univ.pi s) x)
This theorem states that for any non-trivially normed field (`š`), any type `Ī¹` with decidable equality, any normed additively commutative group (`E i`) that is a normed space over `š` for each `i` in `Ī¹`, any set `s` of elements of `E i` for each `i` in `Ī¹`, and any point `x` in `E i` for each `i` in `Ī¹`, if for every `j` in `Ī¹` that is not `i`, `x j` is in the closure of `s j`, then the tangent cone at `x i` in `s i` is mapped to the tangent cone at `x` in the product of all sets `s i` by the linear map that is a single application of `i`. In simpler terms, the tangent cone of a product set includes the tangent cones of each of its constituent sets.
More concisely: If `š` is a non-trivially normed field, `E i` is a normed additively commutative group over `š` for each `i` in the decidably equal index type `Ī¹`, `s i` is a subset of `E i`, and for every `i` and `j` in `Ī¹` with `i ā j`, `x j` is in the closure of `s j`, then the tangent cone of `x i` in `s i` is contained in the linear image of the product of the tangent cones of `x` in each `s i`.
|
mem_tangentCone_of_segment_subset
theorem mem_tangentCone_of_segment_subset :
ā {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ā G] {s : Set G} {x y : G},
segment ā x y ā s ā y - x ā tangentConeAt ā s x
The theorem `mem_tangentCone_of_segment_subset` states that if we have a subset `s` of a real vector space (which itself is a Normed Additive Commutative Group with a Normed Space over the real numbers), and if a line segment from `x` to `y` is completely contained within `s`, then the direction vector from `x` to `y` (obtained as `y - x`) is an element of the tangent cone at the point `x` with respect to the set `s`. In other words, the direction of this segment belongs to the set of all possible direction vectors of line segments that just touch the set `s` at the point `x` and can be extended infinitely in their direction, without leaving `s`.
More concisely: If a line segment between points `x` and `y` in a Normed Additive Commutative Group with a Normed Space is contained in a subset `s`, then the direction vector `y - x` belongs to the tangent cone of `s` at `x`.
|
uniqueDiffOn_Icc
theorem uniqueDiffOn_Icc : ā {a b : ā}, a < b ā UniqueDiffOn ā (Set.Icc a b)
The theorem `uniqueDiffOn_Icc` asserts that for any two real numbers `a` and `b` where `a` is less than `b`, the left-closed right-closed interval from `a` to `b` (denoted as `[a, b]` in mathematics) possesses a unique differential structure. In other words, there is a unique way to do calculus (take derivative, integrate, etc.) on the interval `[a, b]`.
More concisely: For any real numbers `a` < `b`, the interval `[a, b]` has a unique differential structure.
|
tangentConeAt.lim_zero
theorem tangentConeAt.lim_zero :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {y : E} {Ī± : Type u_5} (l : Filter Ī±) {c : Ī± ā š} {d : Ī± ā E},
Filter.Tendsto (fun n => āc nā) l Filter.atTop ā
Filter.Tendsto (fun n => c n ā¢ d n) l (nhds y) ā Filter.Tendsto d l (nhds 0)
This theorem, named `tangentConeAt.lim_zero`, states that under certain conditions, a sequence `d` tends to 0 at infinity. This is in the context of a tangent cone in a normed vector space.
More specifically, it applies to any non-trivially normed field `š`, any normed additive commutative group `E` which is also a normed space over `š`, any element `y` of `E`, and any filter `l` on some type `Ī±`. Given two sequences `c : Ī± ā š` and `d : Ī± ā E`, if the norm of `c` tends to infinity with respect to the filter `l` (`Filter.Tendsto (fun n => āc nā) l Filter.atTop`) and if the sequence obtained by scaling `d` by `c` tends to the neighborhood of `y` with respect to `l` (`Filter.Tendsto (fun n => c n ā¢ d n) l (nhds y)`), then the sequence `d` tends to the neighborhood of 0 (`nhds 0`) with respect to the same filter `l` (`Filter.Tendsto d l (nhds 0)`).
More concisely: If a sequence `c` tends to infinity and another sequence `d` scales with `c` to converge to a neighborhood of `y`, then `d` converges to a neighborhood of 0.
|
uniqueDiffWithinAt_univ
theorem uniqueDiffWithinAt_univ :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {x : E}, UniqueDiffWithinAt š Set.univ x
This theorem, `uniqueDiffWithinAt_univ`, states that for any nontrivially normed field `š` and any normed commutative additive group `E` that is also a normed space over `š`, for any element `x` from `E`, the property `UniqueDiffWithinAt š Set.univ x` holds. In more mathematical terms, this theorem says that for any vector space `E` over a non-trivially normed field `š`, at any point `x` in `E`, the unique differential within the universal set of `E` at `x` exists. This is a key concept in differential geometry and analysis, emphasizing the universality of differential structures within the entire space.
More concisely: For any nontrivially normed field `š` and normed commutative additive group `E` over `š`, at each point `x` in `E`, there exists a unique linear map `df : E ā š` such that the limit `ā(Īµ : ā > 0), ā(h : E), ||h - x|| < Īµ ā ||df h - df x|| < ||h - x||` holds.
|