English
For a given open partial homeomorph f, the local structomorph condition at the source is equivalent to the existence of a G-element e that matches f on the source subset and whose source is contained in f.source.
Русский
Для заданного открытого частичного гомоморфа f условие локального структуроморфа на источнике эквивалентно существованию элемента e∈G, который совпадает с f на источнике и чей источник содержится внутри source f.
LaTeX
$$$ G.IsLocalStructomorphWithinAt f f.source x \iff x \in f.source \to \exists e \in G, e.source \subseteq f.source \land EqOn f e.toFun e.source \land x \in e.source.$$$
Lean4
/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is an open partial homeomorph
and the set we're considering is `f.source`. -/
theorem _root_.OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff {G : StructureGroupoid H}
[ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {x : H} :
G.IsLocalStructomorphWithinAt (⇑f) f.source x ↔
x ∈ f.source →
∃ e : OpenPartialHomeomorph H H, e ∈ G ∧ e.source ⊆ f.source ∧ EqOn f (⇑e) e.source ∧ x ∈ e.source :=
haveI : x ∈ f.source ∪ f.sourceᶜ := by simp_rw [union_compl_self, mem_univ]
f.isLocalStructomorphWithinAt_iff' Subset.rfl this
