hasMFDerivWithinAt — Mathlib

English

A variant of the preceding reformulation focusing on subsets and the containment relations of e.source and f.source.

Русский

Вариант предыдущей формулировки, подчёркивающий подмножества и отношения включения источников e и f.

LaTeX

$$$ \text{OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'}(G, f, s, x) :\ G.IsLocalStructomorphWithinAt f s x \iff x \in s \to \exists e \in G, e.source \subseteq f.source \land EqOn f e.toFun' e.source \land x \in e.source.$$$

Lean4

protected theorem hasMFDerivWithinAt {s x} : HasMFDerivWithinAt I 𝓘(𝕜, E) I s x (ContinuousLinearMap.id _ _) :=
  I.hasMFDerivAt.hasMFDerivWithinAt

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