English
A refinement of the previous equivalence when hs: f.source ⊆ s holds, yielding an explicit bound on how the source of e sits inside f.source in the equivalence.
Русский
Уточнение предыдущего эквивалентности при условии hs: f.source ⊆ s, дающее явное включение источника e в источник f в рамках эквивалентности.
LaTeX
$$$ \text{OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff'}(G, f)\,(hs)\,(hx) : G.IsLocalStructomorphWithinAt f s x \iff x \in s \to \exists e \in G, e.source \subseteq f.source \land EqOn f e.toFun' (s \cap 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 a superset of `f.source`. -/
theorem _root_.OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff' {G : StructureGroupoid H}
[ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {s : Set H} {x : H} (hs : f.source ⊆ s)
(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) e.source ∧ x ∈ e.source :=
by
rw [f.isLocalStructomorphWithinAt_iff hx]
refine imp_congr_right fun _ ↦ exists_congr fun e ↦ and_congr_right fun _ ↦ ?_
refine and_congr_right fun h2e ↦ ?_
rw [inter_eq_right.mpr (h2e.trans hs)]
