Theorems · Theorem · global analysis

StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid

∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ∀ {f : OpenPartialHomeomorph H H}, f ∈ G → ChartedSpace.LiftPropOn Q (↑f) f.source

Defined in: Mathlib.Geometry.Manifold.LocalInvariantProperties
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.univstatement and proof · cited by 3,945
PartialEquiv.sourcestatement · cited by 964
PartialHomeomorph.toPartialEquivstatement · cited by 917
OpenPartialHomeomorph.toPartialHomeomorphstatement · cited by 851
OpenPartialHomeomorph.toFun'statement · cited by 745
OpenPartialHomeomorphstatement and proof · cited by 664
StructureGroupoidstatement and proof · cited by 121
StructureGroupoid.LocalInvariantPropstatement and proof · cited by 64
ChartedSpace.LiftPropOnstatement · cited by 16
StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlasproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

contMDiffOn_of_mem_contDiffGroupoidproof · cited by 1