Theorems · Theorem · global analysis

StructureGroupoid.locality

∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H},
  (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) → e ∈ G

Defined in

Mathlib.Geometry.Manifold.StructureGroupoid

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpace