Theorems · Theorem · global analysis

StructureGroupoid.restr_mem_of_eqOn

∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  {e e' : OpenPartialHomeomorph H H},
  e ∈ G → ∀ {s : Set H}, IsOpen s → Set.EqOn (↑e) (↑e') s → e'.source ∩ s ⊆ e.source → e'.restr s ∈ G

Defined in

Mathlib.Geometry.Manifold.StructureGroupoid

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceClosedUnderRestriction