StructureGroupoid.id_mem_maximalAtlas
theorem StructureGroupoid.id_mem_maximalAtlas :
∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H),
PartialHomeomorph.refl H ∈ StructureGroupoid.maximalAtlas H G
This theorem states that for any given topological space 'H' and any structure groupoid 'G' defined on it, the identity partial homeomorphism on 'H' is always a member of the maximal atlas of the structure groupoid 'G' in this topological space. In other words, in the model space, the identity map is always a part of any maximal collection of charts that covers the entire space and is compatible with the groupoid 'G'.
More concisely: The identity map is always included in any maximal atlas of charts for a given topological space and structure groupoid.
|
ChartedSpace.locallyCompactSpace
theorem ChartedSpace.locallyCompactSpace :
∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
[inst : LocallyCompactSpace H], LocallyCompactSpace M
This theorem states that if a topological space, denoted by `M`, admits an atlas with locally compact charts (denoted by `H`), then the topological space `M` itself is locally compact. In other words, if each point in the space `M` has a neighborhood whose closure is compact in the chart space `H`, then there is a neighborhood of the same point in space `M` whose closure is also compact. This is under the assumption that the chart space `H` is a locally compact space.
More concisely: If a topological space `M` admits an atlas with locally compact charts, then `M` is locally compact.
|
Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.10
theorem Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.10 : ∀ {α : Type u} {a b : α}, (a ∈ {b}) = (a = b)
This theorem asserts that for any type `α` and any elements `a` and `b` of that type, the statement "`a` is in the set containing only `b`" is equivalent to "`a` equals `b`". In mathematical terms, it's stating that for any `a` and `b` in some set `α`, `a` is an element of the singleton set `{b}` if and only if `a` equals `b`.
More concisely: For any type `α` and any `a, b` in `α`, `a` is an element of the singleton set `{b}` if and only if `a = b`.
|
StructureGroupoid.subset_maximalAtlas
theorem StructureGroupoid.subset_maximalAtlas :
∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
(G : StructureGroupoid H) [inst_3 : HasGroupoid M G], atlas H M ⊆ StructureGroupoid.maximalAtlas M G
The theorem "StructureGroupoid.subset_maximalAtlas" states that for any given structure groupoid 'G', all elements from the atlas (set of partial homeomorphisms between a manifold 'M' and a model space 'H') are also elements of the maximal atlas of the structure groupoid 'G' for a manifold 'M'. This is true regardless of the specific types used for 'M' and 'H', as long as 'M' and 'H' are topological spaces and there exists a charted space structure between 'M' and 'H'.
More concisely: For any topological space manifold M and model space H with a charted space structure between them, the atlas (set of partial homeomorphisms between M and H) is included in the maximal atlas of the structure groupoid of M.
|
StructureGroupoid.chart_mem_maximalAtlas
theorem StructureGroupoid.chart_mem_maximalAtlas :
∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
(G : StructureGroupoid H) [inst_3 : HasGroupoid M G] (x : M), chartAt H x ∈ StructureGroupoid.maximalAtlas M G
The theorem `StructureGroupoid.chart_mem_maximalAtlas` states that for any type `H` equipped with a topological space structure, any type `M` equipped with a topological space structure and a charted space structure over `H`, any `StructureGroupoid` `G` over `H`, and any `x` of type `M` which also forms a groupoid with `G`, the preferred chart at point `x` (`chartAt H x`) is an element of the maximal atlas of `M` with respect to the structure groupoid `G` (`StructureGroupoid.maximalAtlas M G`). In other words, every point in a charted space has a chart that is part of the maximal atlas for the associated structure groupoid.
More concisely: For any type equipped with topological and charted space structures, a point forming a groupoid with a given structure groupoid has a preferred chart that belongs to the maximal atlas of the charted space with respect to that structure groupoid.
|
Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.1
theorem Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.1 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋂ i, s i) = ∀ (i : ι), x ∈ s i
This theorem states that for any type `α`, an indexing type `ι`, an element `x` of type `α`, and a function `s` that maps each index to a set of elements of type `α`, the membership of `x` in the intersection of all sets indexed by `ι` (denoted as `⋂ i, s i`) is equivalent to `x` being a member of each set `s i` for all `i` in `ι`. In mathematical terms, an element `x` belongs to the intersection of a collection of sets `(s i)` if and only if `x` belongs to each set `s i` for all `i`.
More concisely: For any type `α`, indexing type `ι`, element `x` of type `α`, and function `s : ι → set α`, `x` lies in the intersection of `(s i)` for all `i` in `ι` if and only if `x` is an element of each `s i`.
|
Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.5
theorem Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.5 :
∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] (x : M), (x ∈ (chartAt H x).source) = True
This theorem states that for any types `H` and `M`, where `H` is a topological space and `M` is a charted space over `H`, and for any point `x` in `M`, it is always true that `x` is contained in the source of the preferred chart at `x`. In other words, in the context of differential geometry, every point in a manifold is always contained in the domain of its associated chart.
More concisely: For every point `x` in a charted space `M` over a topological space `H`, `x` lies in the domain of its preferred chart at `x`.
|
mem_groupoid_of_pregroupoid
theorem mem_groupoid_of_pregroupoid :
∀ {H : Type u} [inst : TopologicalSpace H] {PG : Pregroupoid H} {e : PartialHomeomorph H H},
e ∈ PG.groupoid ↔ PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target
The theorem `mem_groupoid_of_pregroupoid` states that for any type `H` equipped with a topological space structure, a pregroupoid `PG` on `H`, and any partial homeomorphism `e` of `H` onto itself, `e` is a member of the groupoid associated to `PG` if and only if the property defined by `PG` holds both for `e` on its source and for the inverse of `e` on its target.
More concisely: A partial homeomorphism between a topological space and itself is an object in the groupoid of a pregroupoid if and only if it satisfies the pregroupoid relation on both its source and target.
|
chart_mem_atlas
theorem chart_mem_atlas :
∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] (x : M), chartAt H x ∈ atlas H M
The theorem `chart_mem_atlas` asserts that for any topological space `H` and a charted space `M` over `H`, any chart at a point `x` in `M` is an element of the atlas of `M`. The atlas of a charted space is a set of charts that covers the entire space, so this theorem essentially says that each point in the space `M` is covered by at least one chart from the atlas.
More concisely: For any charted space `M` over a topological space `H` and any point `x` in `M`, there exists a chart in the atlas of `M` containing `x`.
|
StructureGroupoid.compatible_of_mem_maximalAtlas
theorem StructureGroupoid.compatible_of_mem_maximalAtlas :
∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
{G : StructureGroupoid H} {e e' : PartialHomeomorph M H},
e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ StructureGroupoid.maximalAtlas M G → e.symm.trans e' ∈ G
This theorem states that for any two elements `e` and `e'` in the maximal atlas of a structure groupoid `G` over a charted space `M`, the transition map from `e` to `e'` (obtained by composing the inverse of `e` and `e'`) is an element of the structure groupoid `G`. Here, `H` and `M` are types equipped with a topological structure, `G` is a structure groupoid on `H`, and `e` and `e'` are partial homeomorphisms from `M` to `H`. This theorem is a fundamental property in the theory of differentiable manifolds, ensuring that changing coordinates between any two charts in the maximal atlas yields a differentiable map.
More concisely: Given two elements `e` and `e'` in the maximal atlas of a structure groupoid `G` over a charted space `M`, the transition map from `e` to `e'` is an element of `G`.
|
Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.9
theorem Mathlib.Geometry.Manifold.ChartedSpace._auxLemma.9 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem states that for all types `α`, sort `ι`, an element `x` of type `α`, and a mapping `s` from `ι` to a set of elements of type `α`, the membership of `x` in the union of all sets `s i` (for each `i` in `ι`) is equivalent to the existence of some `i` in `ι` for which `x` is a member of the set `s i`. In other words, an element belongs to the union of several sets if and only if there exists at least one set among them in which the element is found.
More concisely: For any type `α`, sort `ι`, element `x` of type `α`, and mapping `s` from `ι` to subsets of `α`, the element `x` belongs to the union of sets `s i` if and only if there exists some `i` in `ι` such that `x` is in `s i`.
|
StructureGroupoid.mem_of_eqOnSource
theorem StructureGroupoid.mem_of_eqOnSource :
∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e e' : PartialHomeomorph H H},
e ∈ G → e' ≈ e → e' ∈ G
The theorem `StructureGroupoid.mem_of_eqOnSource` states that for any type `H` with a topological space structure, given a structure groupoid `G` on `H` and two partial homeomorphisms `e` and `e'` from `H` to `H`, if `e` is an element of `G` and `e'` is equivalent to `e` in the sense that they are defined on the same source and their restrictions to this source coincide, then `e'` is also an element of `G`.
More concisely: If `e` is an element of a groupoid `G` on a topological space `H` and `e'` is a partial homeomorphism equivalent to `e` with the same source, then `e'` is also an element of `G`.
|
StructureGroupoid.mem_maximalAtlas_of_mem_groupoid
theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid :
∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H) {f : PartialHomeomorph H H},
f ∈ G → f ∈ StructureGroupoid.maximalAtlas H G
This theorem states that in a given topological space H, for any partial homeomorphism f, if this f is an element of the structure groupoid G, then it also belongs to the maximal atlas of the same topological space H with respect to the structure groupoid G. In other words, every element of a structure groupoid is also part of the maximal atlas of the same topological space under that structure groupoid.
More concisely: In a topological space H with structure groupoid G, every partial homeomorphism f in G is an element of the maximal atlas of H with respect to G.
|
chartAt_self_eq
theorem chartAt_self_eq :
∀ {H : Type u_5} [inst : TopologicalSpace H] {x : H}, chartAt H x = PartialHomeomorph.refl H
This theorem states that in a model space, the preferred chart at any point is always the identity. More formally, for any type `H` equipped with a topological space structure (model space) and for any point `x` in `H`, the chart at `x` (given by the function `chartAt H x`) is equal to the identity on the whole space (given by the function `PartialHomeomorph.refl H`). This means that in the model space, the mapping from points to their corresponding elements (or 'coordinates') under the preferred chart is always the identity, i.e., each point maps to itself.
More concisely: In any model space, the preferred chart at each point is the identity map.
|
mem_chart_target
theorem mem_chart_target :
∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
(x : M), ↑(chartAt H x) x ∈ (chartAt H x).target
The theorem `mem_chart_target` states that for any given point `x` in a topological space `M` which is also a charted space `H`, the image of `x` under the chart at `x`, denoted by `chartAt H x`, is an element of the target set of the chart. In other words, the theorem guarantees that the chart at a given point `x` properly maps `x` into the target space of the chart.
More concisely: For any point x in a charted space H of a topological space M, the image of x under the chart at x lies in the target set of the chart.
|
StructureGroupoid.compatible
theorem StructureGroupoid.compatible :
∀ {H : Type u_5} [inst : TopologicalSpace H] (G : StructureGroupoid H) {M : Type u_6} [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] [inst_3 : HasGroupoid M G] {e e' : PartialHomeomorph M H},
e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G
The theorem `StructureGroupoid.compatible` states that for any topological space `H` and `M`, where `M` is a charted space modeled on `H` with a structure groupoid `G`, and for any two partial homeomorphisms `e` and `e'` from the atlas of `M` to `H`, the transformation from `e'` to the inverse of `e` belongs to the groupoid `G`. This is essentially a compatibility condition of charts in a charted space admitting a structure groupoid, reformulated within the `StructureGroupoid` namespace.
More concisely: Given a charted space `M` modeled on a topological space `H` with a structure groupoid `G`, any two compatible partial homeomorphisms `e` and `e'` from `M` to `H` have inverses related by an element in `G`.
|
PartialHomeomorph.singleton_hasGroupoid
theorem PartialHomeomorph.singleton_hasGroupoid :
∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : PartialHomeomorph α H)
(h : e.source = Set.univ) (G : StructureGroupoid H) [inst_2 : ClosedUnderRestriction G], HasGroupoid α G
The theorem `PartialHomeomorph.singleton_hasGroupoid` states that for a given partial homeomorphism `e` from a topological space `α` into another topological space `H`, if the source of this homeomorphism covers the entire space `α`, then the induced charted space structure on `α` possesses a property known as `HasGroupoid` for any structure groupoid `G` which is closed under restrictions. In simpler terms, if every point in `α` is mapped into `H` by `e`, then `α` has the structure groupoid property with any groupoid that maintains its structure when restricted.
More concisely: If a partial homeomorphism with dense domain from a topological space onto another space preserves the structure groupoid property for any groupoid closed under restrictions, then the domain space has the structure groupoid property with that groupoid.
|
mem_chart_source
theorem mem_chart_source :
∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
[inst_2 : ChartedSpace H M] (x : M), x ∈ (chartAt H x).source
This theorem, named `mem_chart_source`, states that for any topological space `H`, and any charted space `M` over `H`, every point `x` in the charted space `M` is a member of the source set of the chart at `x`. In other words, the chart that maps `M` to `H` is valid at the point `x`, which is to say, `x` is in the domain of the chart.
More concisely: For any charted space `M` over a topological space `H` and any point `x` in `M`, `x` belongs to the source set of the chart at `x`.
|
StructureGroupoid.symm
theorem StructureGroupoid.symm :
∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H},
e ∈ G → e.symm ∈ G
This theorem states that for any given topological space `H`, structure groupoid `G` on `H`, and a partial homeomorphism `e` from `H` to `H`, if `e` is an element of the structure groupoid `G`, then the inverse of the partial homeomorphism `e`, denoted by `PartialHomeomorph.symm e`, also belongs to the structure groupoid `G`. This shows the property of the groupoid that it is closed under taking inverses of its elements.
More concisely: Given a topological space `H`, a structure groupoid `G` on `H`, and a partial homeomorphism `e` in `G`, the inverse `PartialHomeomorph.symm e` is also in `G`.
|
closedUnderRestriction_iff_id_le
theorem closedUnderRestriction_iff_id_le :
∀ {H : Type u} [inst : TopologicalSpace H] (G : StructureGroupoid H),
ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
The theorem `closedUnderRestriction_iff_id_le` states that for any type `H` equipped with a topological structure and any structure groupoid `G` on `H`, the groupoid `G` is closed under restriction if and only if the groupoid `G` contains the trivial restriction-closed groupoid, which only contains partial homeomorphisms equivalent to the restriction of the identity to the various open subsets of `H`. Here, "contains" means that every member of the trivial restriction-closed groupoid is also a member of `G`.
More concisely: A topological groupoid on a type `H` is closed under restriction if and only if it contains the trivial restriction-closed groupoid of partial homeomorphisms equivalent to identity restrictions on open subsets of `H`.
|
ChartedSpace.locallyConnectedSpace
theorem ChartedSpace.locallyConnectedSpace :
∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
[inst : LocallyConnectedSpace H], LocallyConnectedSpace M
This theorem states that if a topological space (denoted by `M`) admits an atlas with locally connected charts (`H`), then the topological space itself is locally connected. In other words, if 'M' can be divided into regions ('H'), where each region is locally connected (i.e., every point in a region can be reached from every other point in the same region without leaving the region), then the entire space 'M' is also locally connected. It's important that both 'H' and 'M' have a topological space structure, and 'H' is locally connected. This theorem bridges the properties of smaller regions of a space with the properties of the space itself.
More concisely: If a topological space is covered by a locally connected atlas, then it is locally connected.
|
chartedSpaceSelf_atlas
theorem chartedSpaceSelf_atlas :
∀ {H : Type u_5} [inst : TopologicalSpace H] {e : PartialHomeomorph H H},
e ∈ atlas H H ↔ e = PartialHomeomorph.refl H
This theorem states that in the context of a trivial `ChartedSpace` structure where a topological space is modeled over itself through the identity, the members of the atlas (which is a set of partial homeomorphisms) are just the identity. In other words, for any type `H` that is a topological space, and any partial homeomorphism `e` of `H` to itself, `e` is a member of the atlas of `H` if and only if `e` is the identity partial homeomorphism on `H`.
More concisely: In the context of a trivial `ChartedSpace` structure over a topological space `H`, the atlas consists exactly of the identity partial homeomorphisms on `H`.
|
StructureGroupoid.le_iff
theorem StructureGroupoid.le_iff :
∀ {H : Type u} [inst : TopologicalSpace H] {G₁ G₂ : StructureGroupoid H}, G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ G₂
This theorem states that for any given type `H` equipped with a `TopologicalSpace` structure, and any two `StructureGroupoid` objects `G₁` and `G₂` of type `H`, `G₁` is less than or equal to `G₂` if and only if every element `e` in `G₁` is also an element in `G₂`. Essentially, this theorem defines the concept of one `StructureGroupoid` being a subset (or equal) to another in the context of topological spaces.
More concisely: For any topological spaces `H` and `G₁`, `G₂` being a subgroupoid of `G₁` (as structures on `H`) if and only if every element in `G₁` is an element in `G₂`.
|