English
For an OpenPartialHomeomorph f : H → H, and G closed under restriction, the local structomorph condition for f within s is equivalent to the existence, for each x ∈ H with x ∈ f.source ∪ s, of an element e ∈ G whose source lies inside f.source and which agrees with f on s ∩ e.source, with x in e.source.
Русский
Для открытого частичного гомоморфа f: H→H и G, замкнутого относительно ограничений, условие локального структурного морфизма для f внутри s эквивалентно существованию для каждого x ∈ H такого, что x ∈ f.source ∪ s, элемента e ∈ G, чья область определения лежит внутри source f и который совпадает с f на s ∩ source e, причём x ∈ source e.
LaTeX
$$$ \text{OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff }(G, f) \, (s, x) : G.IsLocalStructomorphWithinAt f s x \iff x \in s \to ∃ e \in G, e.source \subseteq f.source \land f|_{s\cap e.source} = e|_{s\cap e.source} \land x \in e.source.$$$
Lean4
/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is an open partial homeomorph.
This gives us an `e` that is defined on a subset of `f.source`. -/
theorem _root_.OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff {G : StructureGroupoid H}
[ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {s : Set H} {x : H} (hx : x ∈ f.source ∪ sᶜ) :
G.IsLocalStructomorphWithinAt (⇑f) s x ↔
x ∈ s →
∃ e : OpenPartialHomeomorph H H, e ∈ G ∧ e.source ⊆ f.source ∧ EqOn f (⇑e) (s ∩ e.source) ∧ x ∈ e.source :=
by
constructor
· intro hf h2x
obtain ⟨e, he, hfe, hxe⟩ := hf h2x
refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩
· simp_rw [OpenPartialHomeomorph.restr_source]
exact inter_subset_right.trans interior_subset
· intro x' hx'
exact hfe ⟨hx'.1, hx'.2.1⟩
· rw [f.open_source.interior_eq]
exact Or.resolve_right hx (not_not.mpr h2x)
· intro hf hx
obtain ⟨e, he, _, hfe, hxe⟩ := hf hx
exact ⟨e, he, hfe, hxe⟩
