Theorems · Theorem · global analysis

OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff

∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  (f : OpenPartialHomeomorph H H) {s : Set H} {x : H},
  x ∈ f.source ∪ sᶜ →
    (G.IsLocalStructomorphWithinAt (↑f) s x ↔
      x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source)

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.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceClosedUnderRestriction