DifferentiableOn.diffContOnCl
theorem DifferentiableOn.diffContOnCl :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
DifferentiableOn 𝕜 f (closure s) → DiffContOnCl 𝕜 f s
The given theorem, `DifferentiableOn.diffContOnCl`, establishes that for all types `𝕜`, `E`, and `F`, where `𝕜` is a nontrivially normed field, `E` is a normed additive commutative group and a normed space over `𝕜`, `F` is also a normed additive commutative group and a normed space over `𝕜`, given a function `f` from `E` to `F` and a set `s` of `E`, if the function `f` is differentiable on the closure of `s`, then `f` is continuously differentiable on the closure of `s`. In simpler terms, this theorem states that if a function is differentiable on every point in the smallest closed set containing a particular set, then it is also continuously differentiable on that set.
More concisely: If a function between two normed spaces is differentiable on the closure of a set, then it is continuously differentiable on the closure of that set.
|
diffContOnCl_const
theorem diffContOnCl_const :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {c : F},
DiffContOnCl 𝕜 (fun x => c) s
This theorem, `diffContOnCl_const`, states that for any type 𝕜 that is a non-trivially normed field, any type E and F that are normed additive commutative groups, and with 𝕜 as the normed space for both E and F, for any set s of type E and any constant c of type F, the function which maps any element to the constant c is differentially continuous on the closure of the set s. This means the derivative of this constant function is continuous on the set s.
More concisely: For any non-trivially normed field 𝕜, any normed additive commutative groups E and F with 𝕜 as their common normed space, and any constant c in F, the function mapping every element in the closed set s of E to c is differentially continuous.
|
DiffContOnCl.differentiableAt
theorem DiffContOnCl.differentiableAt :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
{x : E}, DiffContOnCl 𝕜 f s → IsOpen s → x ∈ s → DifferentiableAt 𝕜 f x
The theorem `DiffContOnCl.differentiableAt` states the following: For any field `𝕜` with a non-trivial norm, and any normed additive commutative groups `E` and `F` over `𝕜`, given a function `f` from `E` to `F`, a set `s` of points in `E`, and a point `x` in `E`, if the function `f` is continuously differentiable on the closure of `s`, and `s` is an open set, then if `x` is an element of `s`, the function `f` is differentiable at the point `x`.
More concisely: If `f:` `E` -> `F` is a continuously differentiable function on the closed set `s` ⊆ `E` (in the topology induced by the norms), and `x` ∈ `s` is an interior point, then `f` is differentiable at `x`.
|
DiffContOnCl.sub
theorem DiffContOnCl.sub :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 g s → DiffContOnCl 𝕜 (f - g) s
The theorem `DiffContOnCl.sub` states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F`, and a normed space over `𝕜` for both `E` and `F`, if two functions `f` and `g` from `E` to `F` are differentially continuous on the closure of a set `s` of `E`, then their difference function `(f - g)` is also differentially continuous on the closure of the same set `s`.
More concisely: If two functions between normed spaces are differentially continuous on the closure of a set, then their difference function is also differentially continuous on the closure of that set.
|