Trivialization.mem_source
theorem Trivialization.mem_source :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {x : Z},
x ∈ e.source ↔ proj x ∈ e.baseSet
This theorem states that for any types `B`, `F`, and `Z`, given that `B` and `F` are topological spaces and `Z` is projected onto `B` through a function `proj`, for any trivialization `e` of `F` with respect to `proj` and any element `x` of `Z`, `x` is in the source of the trivialization `e` if and only if the projection of `x` is in the base set of `e`. In the context of differential geometry, this can be interpreted as a relationship between the preimages of points in a topological space and their corresponding points in a trivializing neighborhood.
More concisely: For any types `B`, `F`, and `Z`, given that `B` and `F` are topological spaces, `Z` is projected onto `B` through a function `proj`, and `e` is a trivialization of `F` over `B`, the element `x` of `Z` is in the domain of `e` if and only if `proj(x)` is in the base space of `e`.
|
Trivialization.continuousAt_of_comp_left
theorem Trivialization.continuousAt_of_comp_left :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] {X : Type u_6} [inst_3 : TopologicalSpace X] {f : X → Z} {x : X}
(e : Trivialization F proj),
ContinuousAt (proj ∘ f) x → proj (f x) ∈ e.baseSet → ContinuousAt (↑e ∘ f) x → ContinuousAt f x
The theorem `Trivialization.continuousAt_of_comp_left` states that for any types `B`, `F`, `Z`, and `X`, which are all topological spaces, and any function `f : X → Z`, `proj : Z → B` and a trivialization `e` of `Z` with a function `proj`, if the composition of `proj` and `f` is continuous at a point `x` in `X` and if the projection of `f(x)` belongs to the base set of the trivialization `e`, and if the composition of the inverse of `e` and `f` is also continuous at `x`, then the function `f` is continuous at the point `x`.
In simpler terms, this theorem allows us to infer the continuity of a function `f` at a point `x` by considering the continuity of `f` composed with other functions and verifying that certain conditions hold in the context of a topological trivialization.
More concisely: Given topological spaces B, F, Z, a function f : X → Z, a trivialization e : Z ≃ B with continuous projections, if f ∘ proj is continuous at x, proj(f(x)) is in the base set of e, and the inverse of e ∘ f is continuous at x, then f is continuous at x.
|
Trivialization.mk_symm
theorem Trivialization.mk_symm :
∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (x : B) → Zero (E x)]
(e : Trivialization F Bundle.TotalSpace.proj) {b : B},
b ∈ e.baseSet → ∀ (y : F), { proj := b, snd := e.symm b y } = ↑e.symm (b, y)
The theorem `Trivialization.mk_symm` asserts that for any given set `B` with a topological structure, a set `F` also with a topological structure, a set `E` which is a function space from `B` to some other set with each element of `B` having an associated zero in `E`, a trivialization `e` of the bundle space with projection `Bundle.TotalSpace.proj`, and any element `b` of `B` that belongs to the base set of the trivialization `e`, for any `y` in `F`, the pair `(b, y)` after being transformed by the inverse of the partial homeomorphism associated with `e`, is equal to a pair whose first element is `b` and the second element is the result of applying the inverse of the trivialization `e` at `b` to `y`. This theorem essentially gives a condition under which the inverse of a given trivialization can be fully defined.
More concisely: Given a bundle `B x F` with projection `Bundle.TotalSpace.proj`, a trivialization `e` with inverse `e⁻¹`, and an element `b ∈ B` and `y ∈ F`, the pairs `(b, y)` and `(b, e⁻¹ (e (b, y)))` are equal.
|
Pretrivialization.apply_mk_symm
theorem Pretrivialization.apply_mk_symm :
∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : (x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B},
b ∈ e.baseSet → ∀ (y : F), ↑e { proj := b, snd := e.symm b y } = (b, y)
The theorem `Pretrivialization.apply_mk_symm` states that for every topological spaces `B` and `F`, and a family `E` of `zero` types indexed by `B`, given a pretrivialization `e` of the projection from the total space `Bundle.TotalSpace` to `B`, for any point `b` in the base set of `e`, the composition of the embedding `e` and the inverse of `e` at `b` applied to any point `y` in `F` equals the pair `(b, y)`. This essentially means that the pretrivialization and its inverse form an identity on the base set when applied in succession.
More concisely: For every pretrivialization `e` of a bundle projection to a base space `B`, and for any point `b` in `B` and any point `y` in the fiber `F` over `b`, we have `e (e.inv `b` y) = (b, y)`.
|
Trivialization.proj_symm_apply'
theorem Trivialization.proj_symm_apply' :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F},
b ∈ e.baseSet → proj (↑e.symm (b, x)) = b
The theorem `Trivialization.proj_symm_apply'` states that for any types `B`, `F`, and `Z` with given topological space structures, a projection map `proj` from `Z` to `B`, a trivialization `e` of `F` with respect to `proj`, and any elements `b` in `B` and `x` in `F` such that `b` lies in the base set of `e`, the projection of the inverse image under the partial homeomorphism associated with `e` of the pair `(b, x)` is equal to `b`. In other words, applying our projection after transforming `(b, x)` via the inverse of the partial homeomorphism associated with our trivialization lands us back at `b`.
More concisely: Given a projection map `proj` from a topological space `Z` to `B`, a trivialization `e` of a type `F` with respect to `proj`, and `b` in `B` and `x` in `F` such that `b` is in the base set of `e`, then the projection of `e.partialHomeo.inv.apply (b, x)` is equal to `b`.
|
Pretrivialization.mem_target
theorem Pretrivialization.mem_target :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} (e : Pretrivialization F proj) {x : B × F}, x ∈ e.target ↔ x.1 ∈ e.baseSet
This theorem, "Pretrivialization.mem_target", states that for all types `B`, `F`, and `Z` where `B` and `F` are topological spaces and `proj` is a function from `Z` to `B`, and given a pretrivialization `e` of `F` with respect to `proj` and a pair `x` of `B` and `F`, then `x` is in the target of `e` if and only if the first element of `x` is in the base set of `e`.
More concisely: For any topological spaces B, F, and Z, and a pretrivialization e of F over B with respect to a map proj : Z -> B, the pair (x.1, x) is in the target of e if and only if x.1 is in the base set of e.
|
Trivialization.mem_target
theorem Trivialization.mem_target :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {x : B × F},
x ∈ e.target ↔ x.1 ∈ e.baseSet
This theorem, named `Trivialization.mem_target`, states that for all types `B`, `F`, and `Z` where `B`, `F`, and `Z` are topological spaces and `proj` is a function from `Z` to `B`, given a trivialization `e` of `F` using `proj`, and an ordered pair `x` of type `B × F`, `x` is in the target of the trivialization if and only if the first component of `x` is in the base set of the trivialization. In other words, it relates the membership of an element in the target of a trivialization to the membership of its first component in the base set of the trivialization.
More concisely: For any topological spaces B, F, and Z, and a trivialization e of F over B using a function proj, an element (x, y) of B × F belongs to the target of e if and only if the first component x of x is in the base set of e.
|
Pretrivialization.proj_symm_apply
theorem Pretrivialization.proj_symm_apply :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} (e : Pretrivialization F proj) {x : B × F}, x ∈ e.target → proj (↑e.symm x) = x.1
This theorem states that for any types `B`, `F`, and `Z` that are equipped with the structure of a topological space, and given a function `proj` from `Z` to `B`, a pretrivialization `e` of `F` with respect to `proj`, and a pair `x` of `B` and `F`, if `x` lies in the target of `e`, then applying `proj` to the element obtained by applying the inverse of the partial equivalence associated with `e` to `x` gives back the first component of `x`. In simpler terms, under these conditions, the projection function `proj` undoes the effect of applying the inverse of the partial equivalence on `x` to retrieve its first component.
More concisely: Given a continuous function `proj : Z -> B`, a pretrivialization `e : F -> E` of `F` over `B`, and `x : B x F` such that `x_1 : B` is in the image of `proj` and `x = e.pi._1 x_1 ⊗ x.2`, then `proj (e.pi._2 x) = x_1`.
|
Trivialization.coe_fst'
theorem Trivialization.coe_fst' :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {x : Z},
proj x ∈ e.baseSet → (↑e x).1 = proj x
The theorem `Trivialization.coe_fst'` states that for all types `B`, `F`, and `Z`, given a topological space on `B`, `F`, and `Z`, and a projection function `proj` from `Z` to `B`, if `e` is a trivialization of `F` with respect to `proj` and `x` is an element of `Z` such that the projection of `x` is in the base set of `e`, then the first component of the pair resulting from applying `e` to `x` is equal to the projection of `x`.
In simpler terms, this theorem is about the properties of a mathematical construct called a "trivialization" in the context of topological spaces. It asserts that, under certain conditions, applying a trivialization to an element of a space and then taking the first component of the result, is the same as just projecting the element to another space.
More concisely: Given a trivialization `e` and an element `x` in the domain of `e` with `proj(x)` in the base set, the first component of `e x` equals `proj(x)`.
|
Trivialization.coe_coe
theorem Trivialization.coe_coe :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj), ↑e.toPartialHomeomorph = ↑e
This theorem states that for any types B, F, and Z, where B, F, and Z are topological spaces, and a function `proj` from Z to B, the operation of converting a trivialization of F over proj to a partial homeomorphism and then taking its co-domain (indicated by `↑`) is equivalent to taking the co-domain of the original trivialization. In other words, the process of transforming a trivialization into a partial homeomorphism doesn't change its co-domain.
More concisely: For any types B, F, and Z being topological spaces, and a function `proj` from Z to B, the co-domain of the partial homeomorphism obtained from a trivialization of F over `proj` is equal to the co-domain of the original trivialization.
|
Pretrivialization.mem_source
theorem Pretrivialization.mem_source :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} (e : Pretrivialization F proj) {x : Z}, x ∈ e.source ↔ proj x ∈ e.baseSet
This theorem is stating that for any types `B`, `F`, and `Z`, with `B` and `F` equipped with a topology, and any function `proj` from `Z` to `B`, for a given `Pretrivialization` `e` of `F` with respect to `proj`, an element `x` of `Z` is in the source of the pretrivialization `e` if and only if the projection of `x` using `proj` is in the base set of the pretrivialization `e`. This theorem relates the source of a pretrivialization with its base set through the projection function.
More concisely: For any types `B`, `F` with topologies, and a function `proj` from `Z` to `B`, if `e` is a pretrivialization of `F` with respect to `proj`, then `x` is in the source of `e` if and only if `proj(x)` is in the base set of `e`.
|
Trivialization.tendsto_nhds_iff
theorem Trivialization.tendsto_nhds_iff :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {α : Type u_6} {l : Filter α} {f : α → Z}
{z : Z},
z ∈ e.source →
(Filter.Tendsto f l (nhds z) ↔
Filter.Tendsto (proj ∘ f) l (nhds (proj z)) ∧ Filter.Tendsto (fun x => (↑e (f x)).2) l (nhds (↑e z).2))
The theorem `Trivialization.tendsto_nhds_iff` states that for any types `B`, `F`, and `Z` with `B`, `F`, and `Z` being topological spaces, and given a projection function `proj` from `Z` to `B`, a trivialization `e` of `F` over `proj`, and a filter `l` on a type `α`, a function `f` from `α` to `Z`, and a point `z` in `Z` that belongs to the source of `e`, the function `f` tends to the neighborhood of `z` (i.e., the limit of `f` as it approaches `z` exists) if and only if both the composed function `proj ∘ f` tends to the neighborhood of the projected point `proj z`, and the function that maps `x` to the second component of `e` at `f x` tends to the neighborhood of the second component of `e` at `z`.
More concisely: A function from a filter on a type to a topological space tends to a point in the space if and only if its projection to the base space and the second component function of its trivialization tend to the respective neighborhoods of their targets.
|
Pretrivialization.proj_symm_apply'
theorem Pretrivialization.proj_symm_apply' :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} (e : Pretrivialization F proj) {b : B} {x : F}, b ∈ e.baseSet → proj (↑e.symm (b, x)) = b
The theorem `Pretrivialization.proj_symm_apply'` states that for any types `B`, `F`, and `Z`, with `B` and `F` having a topology, a function `proj` from `Z` to `B`, a pretrivialization `e` of `F` with respect to `proj`, a point `b` in `B`, and a point `x` in `F`, if `b` is in the base set of the pretrivialization `e`, then the projection of the inverse of the partial equivalence associated with `e`, applied to the pair `(b, x)`, is equal to `b`. In simpler terms, this means that the inverse operation of the pretrivialization takes us back to our original point in the base set.
More concisely: For any pretrivialization `e` of a topological space `F` over a base space `B`, with `b` in the base set and `x` in `F`, if `b` is in the image of `e`, then `proj(e.equiv.symm.(apply e.equiv)(b, x)) = b`.
|
Pretrivialization.coe_fst
theorem Pretrivialization.coe_fst :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} (e : Pretrivialization F proj) {x : Z}, x ∈ e.source → (↑e x).1 = proj x
This theorem states that for any given types `B`, `F`, and `Z`, where `B` and `F` are topological spaces, a projection function `proj` from `Z` to `B`, a `Pretrivialization` `e` of `F` with respect to `proj`, and any given `x` of type `Z` that belongs to `e.source`, the first component of the tuple obtained by applying `e` to `x` (denoted (↑e x).1) is equal to the result of applying the projection function `proj` to `x`. Essentially, it asserts that the pretrivialization of a point `x` in its source set preserves the original projection in its first component.
More concisely: For any `B`, `F`, `Z`, `proj`: a continuous function from `Z` to `B`, `Pretrivialization` `e` of `F` over `proj`, and `x` in `e.source`, (↑e x).1 = proj x.
|
Trivialization.coordChange_same_apply
theorem Trivialization.coordChange_same_apply :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {b : B},
b ∈ e.baseSet → ∀ (x : F), e.coordChange e b x = x
The theorem `Trivialization.coordChange_same_apply` states that for any types `B`, `F`, and `Z`, where `B` and `F` are topological spaces and `Z` is a space with a `proj` function mapping to `B`, given a trivialization `e` of `F` with respect to `proj`, and any element `b` in the base set of `e`, the coordinate change induced by the same trivialization `e` at `b` is the identity for any element `x` of `F`. In other words, when the two trivializations in the coordinate change are the same, the coordinate change operation doesn't alter the input `x`.
More concisely: Given a trivialization `e` of a topological space `F` over `B`, and `b` in `B`, the coordinate change of `e` at `b` is the identity function on `F`.
|
Trivialization.coe_fst
theorem Trivialization.coe_fst :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {x : Z},
x ∈ e.source → (↑e x).1 = proj x
The theorem `Trivialization.coe_fst` states that for any types `B`, `F`, and `Z` where `B` and `F` have a topological space structure and `Z` is a source with a projection `proj`, if `x` is an element in the source of a trivialization `e` of `proj`, then the first component of `e` at `x` is equal to the projection of `x`. In other words, this theorem is saying that within the source, a trivialization preserves the projective structure.
More concisely: Given a trivialization `e` of a projection `proj` between topological spaces `B` and `F` over a source `Z`, the first component of `e` at a point `x` in the source equals the projection of `x`, i.e., `e ! x = proj x`.
|
Trivialization.continuousAt_of_comp_right
theorem Trivialization.continuousAt_of_comp_right :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] {X : Type u_6} [inst_3 : TopologicalSpace X] {f : Z → X} {z : Z}
(e : Trivialization F proj), proj z ∈ e.baseSet → ContinuousAt (f ∘ ↑e.symm) (↑e z) → ContinuousAt f z
This theorem states that given a function `f` from a topological space `Z` to another topological space `X`, and a point `z` in `Z`, the continuity of `f` at `z` can be established through a trivialization of `Z` containing `z`. More concretely, if we have a trivialization `e` of `Z` such that the projection of `z` is in the base set of `e`, and the function `f` composed with the inverse of `e` is continuous at the image of `z` under `e`, then `f` is continuous at `z`.
In mathematical terms, if we have a trivialization that locally looks like a product space, and we can show that the function is continuous after changing coordinates using this trivialization, then the function is indeed continuous in the original space.
More concisely: Given a continuous function `f` from a topological space `Z` to `X`, a point `z` in `Z`, and a trivialization `e` of `Z` around `z` such that `f` composed with the inverse of `e` is continuous at `e(z)`, then `f` is continuous at `z`.
|
Pretrivialization.toPartialEquiv_injective
theorem Pretrivialization.toPartialEquiv_injective :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : Nonempty F], Function.Injective Pretrivialization.toPartialEquiv
This theorem states that for any types `B`, `F`, and `Z`, along with topological spaces `B` and `F`, and a mapping `proj` from `Z` to `B`, if type `F` is non-empty, then the function `Pretrivialization.toPartialEquiv`, which is a pretrivialization of `F` with respect to the projection `proj`, is injective. In simpler terms, if there exists at least one element in the fiber space `F`, then no two different pretrivializations map to the same partial equivalence.
More concisely: Given types `B`, `F`, and `Z`, topological spaces `B` and `F`, and a mapping `proj` from `Z` to `B`, if `F` is non-empty then the pretrivialization `Pretrivialization.toPartialEquiv` of `F` with respect to `proj` is an injective function.
|
Trivialization.continuousAt_proj
theorem Trivialization.continuousAt_proj :
∀ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
{proj : Z → B} [inst_2 : TopologicalSpace Z] (e : Trivialization F proj) {x : Z},
x ∈ e.source → ContinuousAt proj x
The theorem `Trivialization.continuousAt_proj` states that for any types `B`, `F`, and `Z` equipped with topological spaces, and a projection function `proj` from `Z` to `B`, given a trivialization `e` of `F` with respect to `proj`, the projection `proj` is continuous at any point `x` in the domain of the trivialization. In other words, as `x` tends towards a particular point in the domain of `e.source`, `proj x` also tends towards `proj` of that particular point. This is a fundamental property in the study of fiber bundles in topology.
More concisely: Given a continuous projection `proj : Z -> B`, a trivialization `e : F ⊥ p → X ⊥ id`, and a point `x ∈ dom e.source`, the function `proj` is continuous at `x`.
|