English
A reformulation of the local invariant property for an OpenPartialHomeomorph f on a superset of its source, giving an explicit characterization in terms of e ∈ G with e.source ⊆ f.source and matching on s ∩ e.source.
Русский
Переформулировка локальной инвариантной свойства для открытого частичного гомоморфа f на надмножестве, которое содержит source f, с явной характеристикой через e ∈ G с e.source ⊆ source f и согласием на s ∩ e.source.
LaTeX
$$$ \text{OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff}(G,f) : G.IsLocalStructomorphWithinAt f s x \iff x \in s \to \exists e \in G, e.source \subseteq f.source \land e.toFun' = f|_{s\cap e.source} \land x \in e.source.$$$
Lean4
theorem hasMFDerivWithinAt_symm {x} (hx : x ∈ range I) :
HasMFDerivWithinAt 𝓘(𝕜, E) I I.symm (range I) x (ContinuousLinearMap.id _ _) :=
⟨I.continuousWithinAt_symm, (hasFDerivWithinAt_id _ _).congr' (fun _y hy => I.rightInvOn hy.1) ⟨hx, mem_range_self _⟩⟩
