Theorems · Theorem · global analysis

UniqueDiffWithinAt.mono_field

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} {𝕜' : Type u_3} [inst_4 : Semiring 𝕜'] [inst_5 : SMul 𝕜 𝕜']
  [inst_6 : Module 𝕜' E] [IsScalarTower 𝕜 𝕜' E], UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜' s x

Assume that E is a normed vector space over semirings 𝕜 ⊆ 𝕜' and that x ∈ s is a point of unique differentiability with respect to the set s and the smaller semiring 𝕜, then x is also a point of unique differentiability with respect to the set s and the larger semiring 𝕜'.

Defined in

Mathlib.Analysis.Calculus.TangentCone.Basic

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommGroupModuleTopologicalSpaceSemiringSMulModuleIsScalarTower