StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp
theorem StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp :
∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) [inst_1 : ClosedUnderRestriction G],
G.LocalInvariantProp G G.IsLocalStructomorphWithinAt
This theorem states that for any topological space `H` and a structure groupoid `G` on `H` that is closed under restriction, the property of being a local structomorphism within `G` is a local invariant property. In other words, if a particular mapping within `G` preserves the structure of `H` in a local sense, this property is preserved even when the mapping is restricted to smaller subsets of `H`.
More concisely: For any topological space H and a closed under restriction structure groupoid G on H, the property of a mapping being a local structomorphism in G is a local invariant property.
|
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source
theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source :
∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
[inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
[inst_4 : TopologicalSpace M'] [inst_5 : 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},
G.LocalInvariantProp G' P →
∀ [inst_6 : HasGroupoid M G],
e ∈ StructureGroupoid.maximalAtlas M G →
x ∈ e.source →
(ChartedSpace.LiftPropWithinAt P g s x ↔
ChartedSpace.LiftPropWithinAt P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
This theorem, named `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source`, states that for any given types `H`, `M`, `H'`, and `M'` with `TopologicalSpace` and `ChartedSpace` structures, along with structure groupoids `G` and `G'`, a partial homeomorphism `e` from `M` to `H`, a predicate `P` that takes a function from `H` to `H'`, a subset of `H`, and an element of `H`, a function `g` from `M` to `M'`, a subset `s` of `M`, and an element `x` of `M`; if `G` is a local invariant property with respect to `G'` and `P`, `M` has a groupoid structure under `G`, `e` is in the maximal atlas of `M` with respect to `G`, and `x` is in the source of `e`, then the property `P` holds within the set `s` at the point `x` under the function `g` if and only if it holds within the preimage of `s` under the inverse of `e` at the image of `x` under `e` under the function `g` composed with the inverse of `e`.
More concisely: Given types `H`, `M`, `H'`, `M'`, structure groupoids `G` and `G'`, a partial homeomorphism `e` from `M` to `H`, a predicate `P`, and assumptions that `G` is a local invariant property with respect to `G'` and `P`, `M` has a groupoid structure under `G`, `e` is in the maximal atlas of `M` with respect to `G`, and `x` is in the source of `e`, the property `P` holds at `x` under `g` if and only if it holds at the preimage of `x` under `e` inverted, composed with `g`, and then mapped back to `H` under `e`.
|
StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas
theorem StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas :
∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop}
[inst_3 : HasGroupoid M G],
G.LocalInvariantProp G Q →
(∀ (y : H), Q id Set.univ y) →
e ∈ StructureGroupoid.maximalAtlas M G → ChartedSpace.LiftPropOn Q (↑e) e.source
The theorem `StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas` asserts that for any topological spaces `H` and `M`, with `M` having a charted space structure with respect to `H` and a groupoid `G`, a partial homeomorphism `e` from `M` to `H`, and a property `Q` of maps from `H` to `H`, sets of `H` and points of `H`, if `Q` is a local invariant property with respect to the groupoid `G` and `Q` holds universally for the identity map of `H`, then if `e` is in the maximal atlas of `M` with respect to the groupoid `G`, the property `Q` lifts on the source of `e` under the embedding of `e`. In simpler terms, if a property holds for all points under the identity map and is invariant under the groupoid, then it holds for all points in the source of any map in the maximal atlas.
More concisely: If `Q` is a local invariant property of maps between topological spaces `H` that holds for all identity maps and is respecting groupoid `G`, then for any charted space `M` with respect to `H`, partial homeomorphism `e` from `M` to `H` in the maximal atlas of `M` with respect to `G`, the property `Q` holds for all points in the source of `e`.
|
StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin
theorem StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin :
∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
{G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
G.LocalInvariantProp G' P →
∀ {s : Set H} {x : H} {f g : H → H'}, (nhdsWithin x s).EventuallyEq f g → f x = g x → (P f s x ↔ P g s x)
This theorem states that for any two types `H` and `H'` equipped with topological spaces, along with respective structure groupoids `G` and `G'`, and a property `P` that is a local invariant of these structure groupoids, then for any set `s` of type `H`, any element `x` of type `H`, and any two functions `f` and `g` from `H` to `H'`, if `f` and `g` are equal within the neighborhood of `x` intersected with `s` (i.e., equal almost everywhere in this neighborhood) and `f(x)` equals `g(x)`, then the property `P` holds for `f` at `x` in `s` if and only if it holds for `g` at `x` in `s`. In other words, the property `P` is invariant under almost-everywhere equality of functions in the neighborhood of a point.
More concisely: If two functions between topological spaces with local invariant property `P` are equal almost everywhere in a neighborhood of a point `x` and have equal values at `x`, then `P` holds for both functions at `x`.
|
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff
theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff :
∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
[inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
[inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
{P : (H → H') → Set H → H → Prop} {s : Set M} {x : M},
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)
The theorem `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff` states that for given topological spaces `H`, `M`, `H'`, `M'` with associated charted spaces and structure groupoids `G` and `G'`, a property `P` of functions from `H` to `H'`, a set `s` of `M` and a point `x` in `M`, if the groupoid `G` has the local invariant property with respect to `G'` and `P`, then for any function `f` from `M` to `M'`, the property `P` holds within `s` at `x` if and only if `f` is continuous within `s` at `x` and `P` holds for the function formed by composing the chart at `f(x)` with `f` and the inverse of the chart at `x`, when restricted to the set obtained by intersecting the target of the chart at `x` with the preimage of the intersection of `s` and the preimage of the source of the chart at `f(x)` under the inverse of the chart at `x`, at the image of `x` under the chart at `x`.
More concisely: Given topological spaces H, M, H', M' with associated charted spaces and structure groupoids G and G', a property P of functions from H to H', a set s of M, and a point x in M, if G has the local invariant property with respect to G' and P, then P holds within s at x if and only if f is continuous within s at x and the composition of the chart at f(x), f, and the inverse chart at x restricts to P at the image of x under the chart at x when applied to the intersection of the target of the chart at x with the preimage of s and the source of the chart at f(x) under the inverse chart at x.
|
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux
theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux :
∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
[inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
[inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
{e e' : PartialHomeomorph M H} {f f' : PartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'}
{s : Set M} {x : M},
G.LocalInvariantProp G' P →
e ∈ StructureGroupoid.maximalAtlas M G →
x ∈ e.source →
e' ∈ StructureGroupoid.maximalAtlas M G →
x ∈ e'.source →
f ∈ StructureGroupoid.maximalAtlas M' G' →
g x ∈ f.source →
f' ∈ StructureGroupoid.maximalAtlas M' G' →
g x ∈ f'.source →
ContinuousWithinAt g s x →
(P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔
P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x))
This theorem is about properties of functions (or "germs") on manifolds. It states that if a certain property of a function `g` is invariant under a structure groupoid (i.e., it remains the same under transformations by the groupoid), then this property does not depend on which atlas or chart we use to describe the source and target manifolds.
In more detail: Given topological spaces `H`, `M`, `H'`, `M'` with corresponding charted spaces `H`, `M`, `H'`, `M'`, and structure groupoids `G`, `G'`, the theorem applies to any two partial homeomorphisms `e` and `e'` from `M` to `H`, and `f` and `f'` from `M'` to `H'`. If the property `P` is invariant under the structure groupoids and all the preconditions are met (the homeomorphisms are part of the maximal atlas, the points `x` and `g x` are in the source of the respective homeomorphisms, and `g` is continuous at `x` within a set `s`), then `P` evaluated at the compositions `(f ∘ g ∘ e.symm)` and `(f' ∘ g ∘ e'.symm)` at points `(e x)` and `(e' x)` respectively are equivalent. This essentially means that the property `P` does not depend on the choice of charts used to describe `g`.
More concisely: Given topological manifolds `M`, `M'` with corresponding atlases and structure groupoids `G`, `G'`, if a property `P` of functions `g : M -> H` and `g' : M' -> H'` is invariant under `G` and `G'`, and if `e : M -> M'`, `e' : M' -> M`, `f : M' -> H'`, and `f' : M -> H'` are compatible partial homeomorphisms such that `g x` and `g' (e x)` belong to the source manifolds and `g` is continuous at `x`, then `P(f ∘ g ∘ e.symm)(e x) ↔ P(f' ∘ g ∘ e'.symm)(x)`.
|
PartialHomeomorph.isLocalStructomorphWithinAt_iff'
theorem PartialHomeomorph.isLocalStructomorphWithinAt_iff' :
∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [inst_1 : ClosedUnderRestriction G]
(f : PartialHomeomorph H H) {s : Set H} {x : H},
f.source ⊆ s →
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)
This theorem states that for a given partial homeomorphism `f` between two topological spaces of type `H` and a structure groupoid `G` of `H` that is closed under restriction, along with a set `s` of `H` and an element `x` of `H`, if the source of `f` is a subset of `s` and `x` is an element of the union of the source of `f` and the complement of `s`, then the function `f` is a local structomorphism at `x` within `s` according to `G` if and only if, when `x` is an element of `s`, there exists an element `e` in `G` such that the source of `e` is a subset of the source of `f`, `f` and `e` are equal on the source of `e`, and `x` is in the source of `e`.
More concisely: For a partial homeomorphism `f` between topological spaces `H` and a closed under restriction groupoid `G` of `H`, `x` in `H`, and subset `s` of `H`, `f` is a local structomorphism of `G` at `x` within `s` if and only if there exists an element `e` in `G` with `x` in the source of `e`, `s` is a subset of the source of `e`, and `f` and `e` agree on their sources.
|
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target
theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target :
∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
[inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
[inst_4 : TopologicalSpace M'] [inst_5 : 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},
G.LocalInvariantProp G' P →
∀ [inst_6 : HasGroupoid M' G'],
f ∈ StructureGroupoid.maximalAtlas M' G' →
g x ∈ f.source →
(ChartedSpace.LiftPropWithinAt P g s x ↔
ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g) s x)
This theorem states that for any topological spaces `H`, `M`, `H'`, `M'` with `H` and `H'` being the model spaces and `M` and `M'` being the spaces being modeled, given two structure groupoids `G` and `G'`, a partial homeomorphism `f` from `M'` to `H'`, a property `P` of a function from `H` to `H'`, a function `g` from `M` to `M'`, and a set `s` in `M`, if `G` is a local invariant property for `G'` and `P`, and `M'` has a groupoid `G'`, and `f` is in the maximal atlas of `M'` with respect to `G'`, and `g(x)` is in the source of `f`, then the property `P` holds within `s` at `x` for `g` if and only if `g` is continuous within `s` at `x` and `P` holds within `s` at `x` for the composition of `f` and `g`. In simpler terms, it asserts a kind of equivalence between the properties of `g` and its image under the homeomorphism `f` within a given set.
More concisely: Given topological spaces H, M, H', M' with model spaces H and H', structure groupoids G and G', a partial homeomorphism f from M' to H', a property P of functions, a function g from M to M', and a set s in M: if G is a local invariant property for G' and P, f is in the maximal atlas of M' with respect to G', g(x) is in the source of f, and s is in the domain of g, then P(g(x)) holds if and only if g is continuous at x and P holds for the composite f ∘ g at x.
|
StructureGroupoid.LocalInvariantProp.liftProp_id
theorem StructureGroupoid.LocalInvariantProp.liftProp_id :
∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
G.LocalInvariantProp G Q → (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftProp Q id
This theorem states that for any types `H` and `M`, where both have a topological space structure, and `M` has a charted space structure relative to `H`, if `G` is a structure groupoid on `H`, and `Q` is a property that is locally invariant under `G`, then if `Q` holds for the identity function on the universal set of `H`, then `Q` can be lifted to the whole space `M` via the identity function.
In more informal terms, if we have a property `Q` that remains unchanged under certain transformations `G` in a local neighborhood on a space `H`, and this property `Q` holds everywhere in `H` for the identity function, then this property `Q` also holds for the entire space `M` which is modeled on `H`, when considered under the identity function.
More concisely: If `H` and `M` are topological spaces with `M` charted over `H`, `G` is a groupoid on `H`, `Q` is a locally invariant property under `G`, and `Q(id_H)` holds, then `Q` holds for the identity function on `M`.
|
PartialHomeomorph.isLocalStructomorphWithinAt_iff
theorem PartialHomeomorph.isLocalStructomorphWithinAt_iff :
∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [inst_1 : ClosedUnderRestriction G]
(f : PartialHomeomorph H H) {s : Set H} {x : H},
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)
The theorem `PartialHomeomorph.isLocalStructomorphWithinAt_iff` states that for any topology `H`, structure groupoid `G` on `H` that is closed under restriction, a partial homeomorphism `f` on `H`, a set `s` in `H`, and a point `x` in `H`, if `x` is in the union of the source of `f` and the complement of `s`, then `f` is a local structomorph within `s` at `x` in the groupoid `G` if and only if, when `x` is in `s`, there exists a structomorph `e` in `G` such that the source of `e` is a subset of the source of `f`, `f` and `e` are equal on the intersection of `s` and the source of `e`, and `x` is in the source of `e`.
More concisely: A partial homeomorphism `f` on a topological space `(H, G)` is a local structomorph within `s` at `x` if and only if, when `x` is in `s`, there exists a structomorph `e` in `G` such that `e` and `f` agree on `s` and `x` is in the source of `e`.
|
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'
theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart' :
∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
[inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
[inst_4 : TopologicalSpace M'] [inst_5 : 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},
G.LocalInvariantProp G' P →
∀ [inst_6 : HasGroupoid M G] [inst_7 : HasGroupoid M' G'],
e ∈ StructureGroupoid.maximalAtlas M G →
x ∈ e.source →
f ∈ StructureGroupoid.maximalAtlas M' G' →
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))
This theorem, `StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart'`, is about properties in the context of topological spaces and their charted representations.
It states that given two topological spaces `M` and `M'` with their respective charted spaces `H` and `H'` and structure groupoids `G` and `G'`, along with a specific property `P` about a function from `H` to `H'`, a function `g` from `M` to `M'`, a subset `s` of `M`, and a point `x` in `M`, as well as partial homeomorphisms `e` and `f` compatible with the structure groupoids `G` and `G'`, respectively, if the local invariant property holds for `G', G` and `P`, and if certain conditions about membership in maximal atlases and source sets are met, then the lift property of `P` at `x` applied to `g` within `s` is equivalent to `g` being continuous at `x` within `s` and the lift property of `P` being satisfied for the composition of `f` and the inverse of `e` applied to `g`, restricted to the preimage of `s` under the inverse of `e`, at the image of `x` under `e`.
More concisely: Given topological spaces `M`, `M'` with charted spaces `H`, `H'`, structure groupoids `G`, `G'`, property `P` on functions from `H` to `H'`, function `g` from `M` to `M'`, subset `s` of `M`, point `x` in `M`, and compatible partial homeomorphisms `e`, `f`, if `G'`, `G`, and `P` satisfy the local invariant property, and if `g` is continuous at `x` in `s` and the lift property of `P` holds for `f ∘ e⁻¹(g)(s)` at `e(x)`, then the lift property of `P` holds for `g` within `s` at `x`.
|
PartialHomeomorph.isLocalStructomorphWithinAt_source_iff
theorem PartialHomeomorph.isLocalStructomorphWithinAt_source_iff :
∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [inst_1 : 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
This theorem, `PartialHomeomorph.isLocalStructomorphWithinAt_source_iff`, states that for any partial homeomorphism `f : PartialHomeomorph H H`, where `H` is a type equipped with a topological space structure and `G` is a structure groupoid on `H` that is closed under restriction, and for any `x : H`, `f` is a local structure morphism within its source set at `x`, if and only if `x` is within the source set of `f` and there exists an element `e` in the groupoid `G` such that the source set of `e` is a subset of the source set of `f`, `f` and `e` are equal on the source set of `e`, and `x` exists in the source of `e`. In simpler terms, it states that `f` mimics the behavior of some element `e` in the groupoid `G` near the point `x` within the source set of `f`.
More concisely: Given a partial homeomorphism `f : PartialHomeomorph H H` on a topological space `H` with a closed under restriction structure groupoid `G`, `f` is a local structure morphism within its source set at a point `x` if and only if there exists an element `e` in `G` with `x` in the source of `e` such that `f` and `e` agree on their sources and restrict to the same set.
|
StructureGroupoid.LocalInvariantProp.congr_set
theorem StructureGroupoid.LocalInvariantProp.congr_set :
∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H']
{G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
G.LocalInvariantProp G' P →
∀ {s t : Set H} {x : H} {f : H → H'}, (nhds x).EventuallyEq s t → (P f s x ↔ P f t x)
This theorem states that for any topological spaces `H` and `H'`, structure groupoids `G` and `G'` on these spaces, and a property `P` that applies to a function from `H` to `H'`, a set in `H`, and a point in `H`, if `P` has the local invariant property under `G` and `G'`, then for any two sets `s` and `t` in `H`, a point `x` in `H`, and a function `f` from `H` to `H'`, if `s` equals `t` in the neighborhood of `x`, then `P` holds for `f`, `s`, and `x` if and only if `P` holds for `f`, `t`, and `x`.
In simpler words, under certain conditions, the property `P` is independent of the exact choice of the neighborhood around `x` - if two sets coincide in a neighborhood of `x`, then either `P` holds for both or for neither.
More concisely: Given topological spaces H and H', structure groupoids G and G', and a property P satisfying local invariance under G and G', if s = t in the neighborhood of x in H, then P(f, s, x) if and only if P(f, t, x), for any function f from H to H' and point x in H.
|
StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas
theorem StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas :
∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {x : M}
{Q : (H → H) → Set H → H → Prop} [inst_3 : HasGroupoid M G],
G.LocalInvariantProp G Q →
(∀ (y : H), Q id Set.univ y) →
e ∈ StructureGroupoid.maximalAtlas M G → x ∈ e.source → ChartedSpace.LiftPropAt Q (↑e) x
This theorem states that for any topological spaces `H` and `M`, with `M` having a `ChartedSpace` structure, a structure groupoid `G` over `H`, a partial homeomorphism `e` from `M` to `H`, an element `x` from `M`, and a property `Q` that applies to a function from `H` to `H`, a subset of `H`, and an element of `H`, if `M` has a `Groupoid` structure associated with `G`, and if `Q` is a local invariant property for `G`, and if `Q` holds for the identity function and all elements of `H`, and if `e` belongs to the maximal atlas of `G` for `M`, and if `x` belongs to the source of `e`, then the lift property at `Q` holds for `e` at `x`. The lift property is a condition used in the definition of a manifold in differential geometry.
More concisely: If `H` is a topological space with a charted space structure, `M` is a topological space with a groupoid structure over `H`, `e` is a partial homeomorphism from `M` to `H` belonging to its maximal atlas, `x` is an element of `M` in the source of `e`, and `Q` is a local invariant property for the groupoid structure that holds for the identity function and all elements of `H`, then the lift property at `Q` holds for `e` at `x`.
|