differentiableWithinAtProp_self_source

English

For a chart I' on E and a map f, the differentiability within at x is equivalent to differentiability of the composed map I' ∘ f at x.

Русский

Для отображения f точка x: DifferentiableWithinAt_PROP 𝓘(𝕜,E) I' f s x эквивалентно DifferentiableWithinAt 𝕜 (I' ∘ f) s x.

LaTeX

$$$ DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x \iff DifferentiableWithinAt 𝕜 (I' \circ f) s x $$$

Lean4

theorem differentiableWithinAtProp_self_source {f : E → H'} {s : Set E} {x : E} :
    DifferentiableWithinAtProp 𝓘(𝕜, E) I' f s x ↔ DifferentiableWithinAt 𝕜 (I' ∘ f) s x := by
  simp_rw [DifferentiableWithinAtProp, modelWithCornersSelf_coe, range_id, inter_univ, modelWithCornersSelf_coe_symm,
    CompTriple.comp_eq, preimage_id_eq, id_eq]

Похожие утверждения