FiberBundle.isOpenMap_proj
theorem FiberBundle.isOpenMap_proj :
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
[inst_4 : FiberBundle F E], IsOpenMap Bundle.TotalSpace.proj
The theorem `FiberBundle.isOpenMap_proj` states that for any types `B` and `F` with corresponding topological spaces `B` and `F`, and for any type map `E : B → Type` with corresponding topological spaces `E b` for any `b : B`, if the total space `Bundle.TotalSpace F E` forms a fiber bundle `F E`, then the canonical projection `Bundle.TotalSpace.proj` from the total space of the fiber bundle to its base space `B` is an open map. In terms of topology, this means that the image of any open set in the total space of the fiber bundle is an open set in the base space when mapped under the projection.
More concisely: If `F E` is a fiber bundle over the base space `B` with total space `Bundle.TotalSpace F E`, then the canonical projection `Bundle.TotalSpace.proj` is an open map from `Bundle.TotalSpace F E` to `B`.
|
Mathlib.Topology.FiberBundle.Basic._auxLemma.6
theorem Mathlib.Topology.FiberBundle.Basic._auxLemma.6 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α}, (a ∈ f ⁻¹' s) = (f a ∈ s)
This theorem, known as `Mathlib.Topology.FiberBundle.Basic._auxLemma.6`, states that for any types `α` and `β`, any function `f` from `α` to `β`, any set `s` of `β` and any element `a` of `α`, the element `a` is in the preimage of set `s` under function `f` if and only if the image of `a` under `f` is in the set `s`. In more mathematical terms, for all `a` in `α`, `a` is in `f^-1(s)` if and only if `f(a)` is in `s`.
More concisely: For any functions $f: \alpha \to \beta$ and sets $s \subseteq \beta$, the preimage $f^{-1}(s) \subseteq \alpha$ contains an element $a \in \alpha$ if and only if the image $f(a) \in s$.
|
Mathlib.Topology.FiberBundle.Basic._auxLemma.3
theorem Mathlib.Topology.FiberBundle.Basic._auxLemma.3 : ∀ {α : Type u} (x : α), (x ∈ Set.univ) = True
This theorem states that for any type `α` and any element `x` of that type, `x` belongs to the universal set of `α`. In other words, every element of a type is always a member of the universal set of that type. This is consistent with the definition of the universal set, which contains all elements of a given type.
More concisely: For any type `α` and any of its elements `x`, `x` is an element of the universal set of `α`.
|
FiberBundleCore.continuous_const_section
theorem FiberBundleCore.continuous_const_section :
∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
(Z : FiberBundleCore ι B F) (v : F),
(∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v) →
Continuous
(let_fun this := fun x => { proj := x, snd := v };
this)
This theorem states that if an element `v` of a fiber bundle `F` is invariant under all coordinate changes between any two indices `i` and `j` for any `x` in the intersection of the base sets of `i` and `j`, then there exists a continuous section of the fiber bundle that maps each point `x` in the base space `B` to the pair `{proj := x, snd := v}`. This theorem is particularly applicable to the zero section of a vector bundle, and also to the identity section of the endomorphism bundle of a vector bundle (though the latter is not yet defined).
More concisely: If an element `v` of a fiber bundle `F` is invariant under all coordinate changes between any two indices on the intersection of their base sets, then there exists a continuous section of `F` mapping each point in the base space to the pair `(x, v)`.
|
FiberBundle.continuousWithinAt_totalSpace
theorem FiberBundle.continuousWithinAt_totalSpace :
∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
[inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
[inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {s : Set X}
{x₀ : X},
ContinuousWithinAt f s x₀ ↔
ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
This theorem gives a characterization of continuous functions at a point and within a set into a fiber bundle. For all types `B`, `F`, and `X` with `X` as a topological space, `B` as a topological space, `F` as a topological space and `E` being a function from `B` to some type, and a topological space over the total space of the bundle `F E`, and a function from `B` to topological spaces over `E b`, given an instance of a fiber bundle `F E`, a function `f` from `X` to the total space of the fiber bundle, a set `s` of `X`, and a point `x₀` in `X`, the function `f` is continuous at point `x₀` within the set `s` if and only if both the projection of `f x` onto the base space and the second element of the trivialization of `f x` at the projection of `f x₀` are also continuous at `x₀` within `s`.
More concisely: A function from a topological space X to a fiber bundle over a topological space B is continuous at a point x\_0 in X within a set s of X if and only if both the projection and the second element of the trivialization of the function at x\_0 are continuous at x\_0 within s.
|
FiberBundleCore.continuous_proj
theorem FiberBundleCore.continuous_proj :
∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
(Z : FiberBundleCore ι B F), Continuous Z.proj
This theorem states that the projection on the base of a fiber bundle, constructed from a fiber bundle core, is continuous. Here, the fiber bundle core is denoted by 'Z', which is a parameterized type involving types 'ι', 'B', and 'F', representing the index type, base space, and typical fiber, respectively. 'B' and 'F' are provided with topological space structures. The theorem assures that no matter what specific structures we choose for 'ι', 'B', and 'F', or for the topological spaces, the projection function 'Z.proj' mapping each point in the total space of the fiber bundle to its base point in 'B', preserves the topology, i.e., is continuous.
More concisely: Given a fiber bundle core Z with types ι, B, and F, and assuming B and F are topological spaces, the projection function Z.proj is continuous.
|
Mathlib.Topology.FiberBundle.Basic._auxLemma.4
theorem Mathlib.Topology.FiberBundle.Basic._auxLemma.4 : ∀ (p : Prop), (p ∧ True) = p
This theorem, denoted as `Mathlib.Topology.FiberBundle.Basic._auxLemma.4`, states that for any proposition `p`, the logical conjunction of `p` and `True` is equivalent to `p`. In other words, `p` and `True` together always return the value of `p`. This is because `True` is a tautology, a statement that is always true, and hence it does not affect the truth value of `p` when conjoined with it.
More concisely: For any proposition `p`, `p` and `True` are logically equivalent.
|
FiberBundleCore.continuous_totalSpaceMk
theorem FiberBundleCore.continuous_totalSpaceMk :
∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
(Z : FiberBundleCore ι B F) (b : B), Continuous (Bundle.TotalSpace.mk b)
The theorem `FiberBundleCore.continuous_totalSpaceMk` states that for any types `ι`, `B` and `F`, where `B` and `F` are topological spaces, and given a fiber bundle core `Z` over these types, the inclusion of a fiber (specified by a point `b` in the base space `B`) into the total space is a continuous map. Here, the total space is the set of all points on all fibers, and `Bundle.TotalSpace.mk b` represents the inclusion map of the fiber at `b` into this total space.
More concisely: For any fiber bundle core `Z` over types `ι`, `B`, and topological space `F`, the inclusion map `Bundle.TotalSpace.mk b : Z b ⊆ Z` is continuous, where `b` is a point in `B` and `Z b` is the fiber over `b`.
|
FiberBundle.continuousAt_totalSpace
theorem FiberBundle.continuousAt_totalSpace :
∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
[inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
[inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {x₀ : X},
ContinuousAt f x₀ ↔
ContinuousAt (fun x => (f x).proj) x₀ ∧
ContinuousAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
This theorem states that a function `f` from a topological space `X` to the total space of a fiber bundle `E` over a base `B` with fiber `F` is continuous at a point `x₀` in `X` if and only if both the projection of `f(x)` to `B` and the second component of the trivialization of `f(x)` at `B` are continuous at `x₀`. In other words, the continuity of `f` at `x₀` is characterized by the continuity of these two functions.
More concisely: A function from a topological space to a fiber bundle is continuous at a point if and only if the projection of its value at that point to the base space and the second component of the trivialization at that point are both continuous.
|
FiberBundleCore.isOpenMap_proj
theorem FiberBundleCore.isOpenMap_proj :
∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
(Z : FiberBundleCore ι B F), IsOpenMap Z.proj
This theorem states that for any fiber bundle core `Z` characterized by index type `ι`, base type `B`, and fiber type `F` with `B` and `F` forming topological spaces, the projection onto the base of the fiber bundle is an open map. In other words, if `U` is an open set in the base space `B`, then its image under the projection map `proj` is also an open set. The projection map `proj` is a function that maps each point of the total space of the fiber bundle to the corresponding point in the base space `B`.
More concisely: For any fiber bundle with base space, fiber type, and index type forming topological spaces, the projection map is an open function.
|
FiberBundleCore.localTrivAsPartialEquiv_trans
theorem FiberBundleCore.localTrivAsPartialEquiv_trans :
∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
(Z : FiberBundleCore ι B F) (i j : ι),
(Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv
This theorem states that for any fiber bundle core `Z`, given two indices `i` and `j` representing two local trivializations, the composition of the inverse of the partial equivalence of the local trivialization at `i` and the partial equivalence of the local trivialization at `j` is equivalent to the partial equivalence of the trivialization change from `i` to `j`. Here, `B` is the base space, `F` is the typical fiber, and `ι` is the index set of trivializations, all with appropriate topological space structures.
More concisely: For any fiber bundle $(B, F, ι, Z)$, given local trivializations $i$ and $j$, the composition of their inverse partial equivalences is equivalent to the partial equivalence of the change of trivializations from $i$ to $j$.
|
FiberBundle.quotientMap_proj
theorem FiberBundle.quotientMap_proj :
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
[inst_4 : FiberBundle F E] [inst_5 : Nonempty F], QuotientMap Bundle.TotalSpace.proj
The theorem `FiberBundle.quotientMap_proj` states that for any type `B`, a type `F`, a function `E` from `B` to some type, given that `B` and `F` are endowed with a topological structure, the total space of the bundle `F E` is also endowed with a topological structure, each fiber `E b` for `b` in `B` is given a topological structure, the bundle `F E` is a fiber bundle, and `F` is nonempty, the canonical projection from the total space of the bundle to the base space `B` is a quotient map.
A quotient map is a function that is surjective and for which a subset of the codomain is open if and only if its preimage is open. This theorem tells us something about the topological properties of fiber bundles: in a fiber bundle, the natural projection that sends each point in the total space to its corresponding point in the base space preserves the topological structure in a very specific way encapsulated by being a quotient map.
More concisely: Given a fiber bundle `F E` over a nonempty base space `B` endowed with topologies, the canonical projection is a quotient map.
|
FiberBundle.continuous_proj
theorem FiberBundle.continuous_proj :
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
[inst_4 : FiberBundle F E], Continuous Bundle.TotalSpace.proj
The theorem `FiberBundle.continuous_proj` states that for any base type `B` (which is a topological space), fiber type `F` (which is also a topological space), and a function `E` from `B` to some type, if the total space `Bundle.TotalSpace F E` is a topological space, and for every `b` in `B`, `E b` is a topological space, and if `F E` is a fiber bundle, then the canonical projection from the total space of the bundle to the base space `B`, denoted by `Bundle.TotalSpace.proj`, is a continuous function. In mathematical terms, it asserts that the projection map of a topological fiber bundle is a continuous function.
More concisely: If `F` is a topological fiber bundle over a topological space `B` with continuous base space maps and continuous total space, then the projection map is continuous.
|
FiberPrebundle.mem_pretrivializationAt_source
theorem FiberPrebundle.mem_pretrivializationAt_source :
∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) (x : E b),
{ proj := b, snd := x } ∈ (a.pretrivializationAt b).source
This theorem states that for any given fiber prebundle `a` over a base space `B` with fiber `F` and total space `E`, a point `b` in `B`, and a point `x` in the fiber `E` over `b`, the pair consisting of `b` and `x`, denoted as `{ proj := b, snd := x }`, is always an element of the source set of the pretrivialization of `a` at `b`. Here, "pretrivialization" refers to an operation in the theory of fiber bundles that simplifies the structure of the bundle in a neighborhood of a given point.
More concisely: For any fiber prebundle `a` over a base space `B` with fiber `F` and total space `E`, given a point `b` in `B` and a point `x` in the fiber `E` over `b`, the pair `{proj := b, snd := x}` is in the source set of the pretrivialization of `a` at `b`.
|
FiberPrebundle.continuousOn_of_comp_right
theorem FiberPrebundle.continuousOn_of_comp_right :
∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) {X : Type u_6} [inst_3 : TopologicalSpace X]
{f : Bundle.TotalSpace F E → X} {s : Set B},
IsOpen s →
(∀ b ∈ s,
ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ Set.univ)) →
ContinuousOn f (Bundle.TotalSpace.proj ⁻¹' s)
This theorem states that for a fiber bundle `E` over a base space `B`, constructed using the `FiberPrebundle` mechanism, the continuity of a function `f` from the total space of the bundle to another topological space `X` on an open set `s` in `B`, can be verified by precomposing `f` at each point with the inverse of the pretrivialization used for the bundle's construction at that point. More specifically, the function `f` is continuous on the pre-image of `s` under the projection from the total space to `B` if and only if for every `b` in `s`, the function `f` composed with the inverse of the pretrivialization at `b`, is continuous on the product of the intersection of `s` and the base set of the pretrivialization at `b` with the universal set in the fiber over `b`.
More concisely: For a fiber bundle in Lean 4 constructed using `FiberPrebundle`, a function from its total space to another topological space is continuous on the pre-image of an open set in the base space if and only if, at each point in the open set, the function composed with the inverse of the bundle's pretrivialization is continuous on the corresponding fiber.
|
FiberBundle.surjective_proj
theorem FiberBundle.surjective_proj :
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
[inst : FiberBundle F E] [inst : Nonempty F], Function.Surjective Bundle.TotalSpace.proj
This theorem states that the projection from the total space of a fiber bundle with a nonempty fiber to its base space is a surjective function. Here, the base space 'B', the fiber 'F', the total space of the bundle 'Bundle.TotalSpace F E', and the space 'E b' for each 'b' in 'B' are all assumed to be topological spaces. The surjectivity means that for every point in the base space, there is a point in the total space of the fiber bundle that maps to it under the projection.
More concisely: The projection map from the total space of a fiber bundle to its base space is a surjection.
|
FiberBundle.exists_trivialization_Icc_subset
theorem FiberBundle.exists_trivialization_Icc_subset :
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
[inst_4 : ConditionallyCompleteLinearOrder B] [inst_5 : OrderTopology B] [inst_6 : FiberBundle F E] (a b : B),
∃ e, Set.Icc a b ⊆ e.baseSet
The theorem `FiberBundle.exists_trivialization_Icc_subset` asserts that for any given types `B` and `F`, where `B` is a conditionally complete linear order with a topology and `F` is another type with a topology, if `E` is a fiber bundle over `B` (with `E b` being each fiber's type having a topology), then there exists a trivialization `e` such that any closed interval from `a` to `b` in `B` (denoted by `Set.Icc a b`) is a subset of the base set of this trivialization `e`. In other words, for any closed interval in the base space of a fiber bundle, we can find a trivialization (a homeomorphism between the fiber bundle and the product of its base and fiber spaces) where the closed interval is included in the trivialization's underlying set.
More concisely: Given a fiber bundle E over a conditionally complete linear order B with a topology, for any closed interval Icc a b in B, there exists a trivialization e of E such that Icc a b is a subset of the domain of e.
|