FiberBundle.Prod.inducing_diag
theorem FiberBundle.Prod.inducing_diag :
ā {B : Type u_1} (Fā : Type u_2) (Eā : B ā Type u_3) (Fā : Type u_4) (Eā : B ā Type u_5)
[inst : TopologicalSpace (Bundle.TotalSpace Fā Eā)] [inst_1 : TopologicalSpace (Bundle.TotalSpace Fā Eā)],
Inducing fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
The theorem `FiberBundle.Prod.inducing_diag` states that for any type `B` and any fiber bundles `Eā` and `Eā` over `B` with corresponding total spaces `Fā` and `Fā`, the diagonal map that takes a point in the fiberwise product of `Eā` and `Eā` to a pair of points in `Fā` and `Fā` (with the same projection to `B`) is inducing. Here, inducing refers to the property that the map induces the same topology on its source space as the subspace topology on its image under the map, in the target space.
More concisely: The diagonal map from the fiberwise product of two fiber bundles over a base space to the product of their total spaces is a topological embedding.
|
Mathlib.Topology.FiberBundle.Constructions._auxLemma.4
theorem Mathlib.Topology.FiberBundle.Constructions._auxLemma.4 :
ā {Ī± : Type u} {Ī² : Type v} {f : Ī± ā Ī²} {s : Set Ī²} {a : Ī±}, (a ā f ā»Ā¹' s) = (f a ā s)
This theorem, named `Mathlib.Topology.FiberBundle.Constructions._auxLemma.4`, states that for any types `Ī±` and `Ī²`, a function `f` from `Ī±` to `Ī²`, a set `s` of elements of type `Ī²`, and an element `a` of type `Ī±`, the statement "element `a` is in the preimage of set `s` under function `f`" is equivalent to the statement "the image of `a` under function `f` is in the set `s`".
In mathematical terms, this theorem corresponds to the basic definition of the preimage of a set under a function: $a \in f^{-1}(s)$ if and only if $f(a) \in s$.
More concisely: For any function $f: \alpha \to \beta$ and sets $s \subseteq \beta$ and $a \in \alpha$, $a \in f^{-1}(s)$ if and only if $f(a) \in s$.
|
pullbackTopology_def
theorem pullbackTopology_def :
ā {B : Type u_1} (F : Type u_2) (E : B ā Type u_3) {B' : Type u_4} (f : B' ā B) [inst : TopologicalSpace B']
[inst_1 : TopologicalSpace (Bundle.TotalSpace F E)],
pullbackTopology F E f =
TopologicalSpace.induced Bundle.TotalSpace.proj inst ā
TopologicalSpace.induced (Bundle.Pullback.lift f) inst_1
This theorem states that for any types `B`, `F`, `E`, `B'`, a function `f` from `B'` to `B`, and provided `B'` and the total space of the bundle `F E` are equipped with their respective topological spaces, the pullback topology of `F E` along `f` is equivalent to the infimum (greatest lower bound) of the topologies induced by the projection from the total space of the bundle `F E` to `B`, and the lift of the base map `f` to the total spaces. In other words, the pullback topology is the coarsest topology that makes both the projection and the lift continuous.
More concisely: The pullback topology of a continuous bundle map and a continuous function from the base space to the fiber space is the coarsest topology on the fiber space making both the bundle projection and the lifted function continuous.
|