English
A function f : H → H is a local structomorph within a set s at a point x if, whenever x ∈ s, there exists a G-structure e with source in H such that f agrees with e on s ∩ source and x belongs to the source of e.
Русский
Функция f: H→H является локальным структуромортом внутри множества s в точке x, если при условии x ∈ s существует элемент-структурообменник e с источником в H, на котором f совпадает с e на s ∩ source и x ∈ source e.
LaTeX
$$$ \text{IsLocalStructomorphWithinAt}(f, s, x) \;:\; x \in s \rightarrow \exists e \in G, \; e.source \subseteq H, \; f|_{s \cap e.source} = e|_{s \cap e.source} \land x \in e.source.$$$
Lean4
/-- A function from a model space `H` to itself is a local structomorphism, with respect to a
structure groupoid `G` for `H`, relative to a set `s` in `H`, if for all points `x` in the set, the
function agrees with a `G`-structomorphism on `s` in a neighbourhood of `x`. -/
def IsLocalStructomorphWithinAt (f : H → H) (s : Set H) (x : H) : Prop :=
x ∈ s → ∃ e : OpenPartialHomeomorph H H, e ∈ G ∧ EqOn f e.toFun (s ∩ e.source) ∧ x ∈ e.source
