Local properties invariant under a groupoid

We study properties of a triple (g, s, x) where g is a function between two spaces H and H', s is a subset of H and x is a point of H. Our goal is to register how such a property should behave to make sense in charted spaces modelled on H and H'.

The main examples we have in mind are the properties "g is differentiable at x within s", or "g is smooth at x within s". We want to develop general results that, when applied in these specific situations, say that the notion of smooth function in a manifold behaves well under restriction, intersection, is local, and so on.

Main definitions

• LocalInvariantProp G G' P says that a property P of a triple (g, s, x) is local, and invariant under composition by elements of the groupoids G and G' of H and H' respectively.
• ChartedSpace.LiftPropWithinAt (resp. LiftPropAt, LiftPropOn and LiftProp): given a property P of (g, s, x) where g : H → H', define the corresponding property for functions M → M' where M and M' are charted spaces modelled respectively on H and H'. We define these properties within a set at a point, or at a point, or on a set, or in the whole space. This lifting process (obtained by restricting to suitable chart domains) can always be done, but it only behaves well under locality and invariance assumptions.

Given hG : LocalInvariantProp G G' P, we deduce many properties of the lifted property on the charted spaces. For instance, hG.liftPropWithinAt_inter says that P g s x is equivalent to P g (s ∩ t) x whenever t is a neighborhood of x.

Implementation notes

We do not use dot notation for properties of the lifted property. For instance, we have hG.liftPropWithinAt_congr saying that if LiftPropWithinAt P g s x holds, and g and g' coincide on s, then LiftPropWithinAt P g' s x holds. We can't call it LiftPropWithinAt.congr as it is in the namespace associated to LocalInvariantProp, not in the one for LiftPropWithinAt.

structure StructureGroupoid.LocalInvariantProp {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] (G : StructureGroupoid H) (G' : StructureGroupoid H') (P : (H → H') → Set H → H → Prop) : Prop

Structure recording good behavior of a property of a triple (f, s, x) where f is a function, s a set and x a point. Good behavior here means locality and invariance under given groupoids (both in the source and in the target). Given such a good behavior, the lift of this property to charted spaces admitting these groupoids will inherit the good behavior.

• is_local : ∀ {s : Set H} {x : H} {u : Set H} {f : H → H'}, IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)
• right_invariance' : ∀ {s : Set H} {x : H} {f : H → H'} {e : PartialHomeomorph H H}, e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• congr_of_forall : ∀ {s : Set H} {x : H} {f g : H → H'}, (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x
• left_invariance' : ∀ {s : Set H} {x : H} {f : H → H'} {e' : PartialHomeomorph H' H'}, e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x

theorem StructureGroupoid.LocalInvariantProp.is_local {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (self : G.LocalInvariantProp G' P) {s : Set H} {x : H} {u : Set H} {f : H → H'} : IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)

theorem StructureGroupoid.LocalInvariantProp.right_invariance' {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (self : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e : PartialHomeomorph H H} : e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

theorem StructureGroupoid.LocalInvariantProp.congr_of_forall {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (self : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} : (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x

theorem StructureGroupoid.LocalInvariantProp.left_invariance' {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (self : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e' : PartialHomeomorph H' H'} : e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x

theorem StructureGroupoid.LocalInvariantProp.congr_set {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {t : Set H} {x : H} {f : H → H'} (hu : s =ᶠ[nhds x] t) : P f s x ↔ P f t x

theorem StructureGroupoid.LocalInvariantProp.is_local_nhds {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {u : Set H} {x : H} {f : H → H'} (hu : u ∈ nhdsWithin x s) : P f s x ↔ P f (s ∩ u) x

theorem StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) : P f s x ↔ P g s x

theorem StructureGroupoid.LocalInvariantProp.congr_nhdsWithin {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) (hP : P f s x) : P g s x

theorem StructureGroupoid.LocalInvariantProp.congr_nhdsWithin' {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) (hP : P g s x) : P f s x

theorem StructureGroupoid.LocalInvariantProp.congr_iff {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h : f =ᶠ[nhds x] g) : P f s x ↔ P g s x

theorem StructureGroupoid.LocalInvariantProp.congr {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h : f =ᶠ[nhds x] g) (hP : P f s x) : P g s x

theorem StructureGroupoid.LocalInvariantProp.congr' {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {g : H → H'} (h : f =ᶠ[nhds x] g) (hP : P g s x) : P f s x

theorem StructureGroupoid.LocalInvariantProp.left_invariance {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e' : PartialHomeomorph H' H'} (he' : e' ∈ G') (hfs : ContinuousWithinAt f s x) (hxe' : f x ∈ e'.source) : P (↑e' ∘ f) s x ↔ P f s x

theorem StructureGroupoid.LocalInvariantProp.right_invariance {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e : PartialHomeomorph H H} (he : e ∈ G) (hxe : x ∈ e.source) : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P f s x

theorem ChartedSpace.liftPropWithinAt_iff' {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) (x : M) : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

structure ChartedSpace.LiftPropWithinAt {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) (x : M) : Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property in a charted space, by requiring that it holds at the preferred chart at this point. (When the property is local and invariant, it will in fact hold using any chart, see liftPropWithinAt_indep_chart). We require continuity in the lifted property, as otherwise one single chart might fail to capture the behavior of the function.

• continuousWithinAt : ContinuousWithinAt f s x
• prop : P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

theorem ChartedSpace.LiftPropWithinAt.continuousWithinAt {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {s : Set M} {x : M} (self : ChartedSpace.LiftPropWithinAt P f s x) : ContinuousWithinAt f s x

theorem ChartedSpace.LiftPropWithinAt.prop {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {s : Set M} {x : M} (self : ChartedSpace.LiftPropWithinAt P f s x) : P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

def ChartedSpace.LiftPropOn {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) : Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of functions on sets in a charted space, by requiring that it holds around each point of the set, in the preferred charts.

Equations

• ChartedSpace.LiftPropOn P f s = ∀ x ∈ s, ChartedSpace.LiftPropWithinAt P f s x

def ChartedSpace.LiftPropAt {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (x : M) : Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of a function at a point in a charted space, by requiring that it holds in the preferred chart.

Equations

• ChartedSpace.LiftPropAt P f x = ChartedSpace.LiftPropWithinAt P f Set.univ x

theorem ChartedSpace.liftPropAt_iff {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M} : ChartedSpace.LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)

def ChartedSpace.LiftProp {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') : Prop

Given a property of germs of functions and sets in the model space, then one defines a corresponding property of a function in a charted space, by requiring that it holds in the preferred chart around every point.

Equations

• ChartedSpace.LiftProp P f = ∀ (x : M), ChartedSpace.LiftPropAt P f x

theorem ChartedSpace.liftProp_iff {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} : ChartedSpace.LiftProp P f ↔ Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)

theorem StructureGroupoid.liftPropWithinAt_univ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {x : M} : ChartedSpace.LiftPropWithinAt P g Set.univ x ↔ ChartedSpace.LiftPropAt P g x

theorem StructureGroupoid.liftPropOn_univ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} : ChartedSpace.LiftPropOn P g Set.univ ↔ ChartedSpace.LiftProp P g

theorem StructureGroupoid.liftPropWithinAt_self {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {P : (H → H') → Set H → H → Prop} {f : H → H'} {s : Set H} {x : H} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x

theorem StructureGroupoid.liftPropWithinAt_self_source {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : H → M'} {s : Set H} {x : H} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f) s x

theorem StructureGroupoid.liftPropWithinAt_self_target {H : Type u_1} {M : Type u_2} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} {f : M → H'} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) {f : M → M'} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)

LiftPropWithinAt P f s x is equivalent to a definition where we restrict the set we are considering to the domain of the charts at x and f x.

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux {H : Type u_1} {M : Type u_2} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (g : M → H') (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) (he' : e' ∈ StructureGroupoid.maximalAtlas M G) (xe' : x ∈ e'.source) : P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2 {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : PartialHomeomorph M' H'} {f' : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) (g : H → M') {x : H} {s : Set H} (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hf' : f' ∈ StructureGroupoid.maximalAtlas M' G') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) : P (↑f ∘ g) s x ↔ P (↑f' ∘ g) s x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux {H : Type u_1} {H' : Type u_3} {M' : Type u_4} {X : Type u_5} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace X] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : PartialHomeomorph M' H'} {f' : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {g : X → M'} {e : PartialHomeomorph X H} {x : X} {s : Set X} (xe : x ∈ e.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hf' : f' ∈ StructureGroupoid.maximalAtlas M' G') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) : P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} {f : PartialHomeomorph M' H'} {f' : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) (he' : e' ∈ StructureGroupoid.maximalAtlas M G) (xe' : x ∈ e'.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hf' : f' ∈ StructureGroupoid.maximalAtlas M' G') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) : P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

If a property of a germ of function g on a pointed set (s, x) is invariant under the structure groupoid (by composition in the source space and in the target space), then expressing it in charted spaces does not depend on the element of the maximal atlas one uses both in the source and in the target manifolds, provided they are defined around x and g x respectively, and provided g is continuous within s at x (otherwise, the local behavior of g at x can not be captured with a chart in the target).

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {f : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) [HasGroupoid M G] (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

A version of liftPropWithinAt_indep_chart, only for the source.

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) [HasGroupoid M' G'] (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g) s x

A version of liftPropWithinAt_indep_chart, only for the target.

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart' {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {f : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

A version of liftPropWithinAt_indep_chart, that uses LiftPropWithinAt on both sides.

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : PartialHomeomorph M H} {f : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ StructureGroupoid.maximalAtlas M G) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (h : ChartedSpace.LiftPropOn P g s) {y : H} (hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)) : P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter' {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {t : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (ht : t ∈ nhdsWithin x s) : ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {t : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (ht : t ∈ nhds x) : ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_liftPropWithinAt {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (hs : s ∈ nhds x) : ChartedSpace.LiftPropAt P g x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropAt P g x) (hs : s ∈ nhds x) : ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h : ∀ x ∈ s, ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g (s ∩ u)) : ChartedSpace.LiftPropOn P g s

theorem StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} (hG : G.LocalInvariantProp G' P) (h : ∀ (x : M), ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g u) : ChartedSpace.LiftProp P g

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[nhdsWithin x s] g) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : g' =ᶠ[nhdsWithin x s] g) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : g' =ᶠ[nhds x] g) : ChartedSpace.LiftPropAt P g' x ↔ ChartedSpace.LiftPropAt P g x

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropAt P g x) (h₁ : g' =ᶠ[nhds x] g) : ChartedSpace.LiftPropAt P g' x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_congr {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropOn P g s) (h₁ : ∀ y ∈ s, g' y = g y) : ChartedSpace.LiftPropOn P g' s

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {g' : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h₁ : ∀ y ∈ s, g' y = g y) : ChartedSpace.LiftPropOn P g' s ↔ ChartedSpace.LiftPropOn P g s

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {t : Set M} {x : M} (mono_of_mem : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ nhdsWithin x t → P f s x → P f t x) (h : ChartedSpace.LiftPropWithinAt P g s x) (hst : s ∈ nhdsWithin x t) : ChartedSpace.LiftPropWithinAt P g t x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {t : Set M} {x : M} (mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : ChartedSpace.LiftPropWithinAt P g s x) (hts : t ⊆ s) : ChartedSpace.LiftPropWithinAt P g t x

theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : ChartedSpace.LiftPropAt P g x) : ChartedSpace.LiftPropWithinAt P g s x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_mono {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {t : Set M} (mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : ChartedSpace.LiftPropOn P g t) (hst : s ⊆ t) : ChartedSpace.LiftPropOn P g s

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_liftProp {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} (mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : ChartedSpace.LiftProp P g) : ChartedSpace.LiftPropOn P g s

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) (hx : x ∈ e.source) : ChartedSpace.LiftPropAt Q (↑e) x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) : ChartedSpace.LiftPropOn Q (↑e) e.source

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] {x : H} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) (hx : x ∈ e.target) : ChartedSpace.LiftPropAt Q (↑e.symm) x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) : ChartedSpace.LiftPropOn Q (↑e.symm) e.target

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_chart {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropAt Q (↑(chartAt H x)) x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_chart {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropOn Q (↑(chartAt H x)) (chartAt H x).source

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropAt Q (↑(chartAt H x).symm) (↑(chartAt H x) x)

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropOn Q (↑(chartAt H x).symm) (chartAt H x).target

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {f : PartialHomeomorph H H} (hf : f ∈ G) {x : H} (hx : x ∈ f.source) : ChartedSpace.LiftPropAt Q (↑f) x

theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {f : PartialHomeomorph H H} (hf : f ∈ G) : ChartedSpace.LiftPropOn Q (↑f) f.source

theorem StructureGroupoid.LocalInvariantProp.liftProp_id {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftProp Q id

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {U : TopologicalSpace.Opens M} (f : M → M') (x : ↥U) : ChartedSpace.LiftPropAt P f ↑x ↔ ChartedSpace.LiftPropAt P (f ∘ Subtype.val) x

theorem StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {U : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M} (hUV : U ≤ V) (f : ↥V → M') (x : ↥U) : ChartedSpace.LiftPropAt P f (Set.inclusion hUV x) ↔ ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x

theorem StructureGroupoid.LocalInvariantProp.liftProp_subtype_val {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (U : TopologicalSpace.Opens M) : ChartedSpace.LiftProp Q Subtype.val

theorem StructureGroupoid.LocalInvariantProp.liftProp_inclusion {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {U : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M} (hUV : U ≤ V) : ChartedSpace.LiftProp Q (Set.inclusion hUV)

def StructureGroupoid.IsLocalStructomorphWithinAt {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) (f : H → H) (s : Set H) (x : H) : Prop

A function from a model space H to itself is a local structomorphism, with respect to a structure groupoid G for H, relative to a set s in H, if for all points x in the set, the function agrees with a G-structomorphism on s in a neighbourhood of x.

Equations

• G.IsLocalStructomorphWithinAt f s x = (x ∈ s → ∃ e ∈ G, Set.EqOn f (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source)

theorem StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) [ClosedUnderRestriction G] : G.LocalInvariantProp G G.IsLocalStructomorphWithinAt

For a groupoid G which is ClosedUnderRestriction, being a local structomorphism is a local invariant property.

theorem PartialHomeomorph.isLocalStructomorphWithinAt_iff {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {s : Set H} {x : H} (hx : 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 a partial homeomorph. This gives us an e that is defined on a subset of f.source.

theorem PartialHomeomorph.isLocalStructomorphWithinAt_iff' {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {s : Set H} {x : H} (hs : f.source ⊆ s) (hx : x ∈ f.source ∪ sᶜ) : G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source

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

theorem PartialHomeomorph.isLocalStructomorphWithinAt_source_iff {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : PartialHomeomorph 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 a partial homeomorph and the set we're considering is f.source.

theorem StructureGroupoid.HasGroupoid.comp {H₁ : Type u_6} [TopologicalSpace H₁] {H₂ : Type u_7} [TopologicalSpace H₂] {H₃ : Type u_8} [TopologicalSpace H₃] [ChartedSpace H₁ H₂] [ChartedSpace H₂ H₃] {G₁ : StructureGroupoid H₁} [HasGroupoid H₂ G₁] [ClosedUnderRestriction G₁] (G₂ : StructureGroupoid H₂) [HasGroupoid H₃ G₂] (H : ∀ e ∈ G₂, ChartedSpace.LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source) : HasGroupoid H₃ G₁