Theorems · Theorem · global analysis

OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff

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

A slight reformulation of IsLocalStructomorphWithinAt when f is an open partial homeomorph and the set we're considering is f.source.

Defined in

Mathlib.Geometry.Manifold.LocalInvariantProperties

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceClosedUnderRestriction