Trivializations

Main definitions

Basic definitions

• Trivialization F p : structure extending local homeomorphisms, defining a local trivialization of a topological space Z with projection p and fiber F.

• Pretrivialization F proj : trivialization as a local equivalence, mainly used when the topology on the total space has not yet been defined.

Operations on bundles

We provide the following operations on Trivializations.

• Trivialization.compHomeomorph: given a local trivialization e of a fiber bundle p : Z → B and a homeomorphism h : Z' ≃ₜ Z, returns a local trivialization of the fiber bundle p ∘ h.

Implementation notes

Previously, in mathlib, there was a structure topological_vector_bundle.trivialization which extended another structure topological_fiber_bundle.trivialization by a linearity hypothesis. As of PR leanprover-community/mathlib#17359, we have changed this to a single structure Trivialization (no namespace), together with a mixin class Trivialization.IsLinear.

This permits all the data of a vector bundle to be held at the level of fiber bundles, so that the same trivializations can underlie an object's structure as (say) a vector bundle over ℂ and as a vector bundle over ℝ, as well as its structure simply as a fiber bundle.

This might be a little surprising, given the general trend of the library to ever-increased bundling. But in this case the typical motivation for more bundling does not apply: there is no algebraic or order structure on the whole type of linear (say) trivializations of a bundle. Indeed, since trivializations only have meaning on their base sets (taking junk values outside), the type of linear trivializations is not even particularly well-behaved.

structure Pretrivialization {B : Type u_2} (F : Type u_3) {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] (proj : Z → B) extends LocalEquiv : Type (max (max u_2 u_3) u_5)

• toFun : Z → B × F
• invFun : B × F → Z
• source : Set Z
• target : Set (B × F)
• map_source' : ∀ ⦃x : Z⦄, x ∈ s.source → ↑s.toLocalEquiv x ∈ s.target
• map_target' : ∀ ⦃x : B × F⦄, x ∈ s.target → LocalEquiv.invFun s.toLocalEquiv x ∈ s.source
• left_inv' : ∀ ⦃x : Z⦄, x ∈ s.source → LocalEquiv.invFun s.toLocalEquiv (↑s.toLocalEquiv x) = x
• right_inv' : ∀ ⦃x : B × F⦄, x ∈ s.target → ↑s.toLocalEquiv (LocalEquiv.invFun s.toLocalEquiv x) = x
• open_target : IsOpen s.target
• baseSet : Set B
• open_baseSet : IsOpen s.baseSet
• source_eq : s.source = proj ⁻¹' s.baseSet
• target_eq : s.target = s.baseSet ×ˢ Set.univ
• proj_toFun : ∀ (p : Z), p ∈ s.source → (↑s.toLocalEquiv p).fst = proj p

This structure contains the information left for a local trivialization (which is implemented below as Trivialization F proj) if the total space has not been given a topology, but we have a topology on both the fiber and the base space. Through the construction topological_fiber_prebundle F proj it will be possible to promote a Pretrivialization F proj to a Trivialization F proj.

def Pretrivialization.toFun' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : Z → B × F

Coercion of a pretrivialization to a function. We don't use e.toFun in the CoeFun instance because it is actually e.toLocalEquiv.toFun, so simp will apply lemmas about toLocalEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

instance Pretrivialization.instCoeFunPretrivializationForAllProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} : CoeFun (Pretrivialization F proj) fun x => Z → B × F

theorem Pretrivialization.ext' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) (h₁ : e.toLocalEquiv = e'.toLocalEquiv) (h₂ : e.baseSet = e'.baseSet) : e = e'

theorem Pretrivialization.ext {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} {e : Pretrivialization F proj} {e' : Pretrivialization F proj} (h₁ : ∀ (x : Z), ↑e x = ↑e' x) (h₂ : ∀ (x : B × F), ↑(LocalEquiv.symm e.toLocalEquiv) x = ↑(LocalEquiv.symm e'.toLocalEquiv) x) (h₃ : e.baseSet = e'.baseSet) : e = e'

theorem Pretrivialization.toLocalEquiv_injective {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [Nonempty F] : Function.Injective Pretrivialization.toLocalEquiv

If the fiber is nonempty, then the projection to

@[simp]

theorem Pretrivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑e.toLocalEquiv = ↑e

@[simp]

theorem Pretrivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : (↑e x).fst = proj x

theorem Pretrivialization.mem_source {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} : x ∈ e.source ↔ proj x ∈ e.baseSet

theorem Pretrivialization.coe_fst' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (↑e x).fst = proj x

theorem Pretrivialization.eqOn {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : Set.EqOn (Prod.fst ∘ ↑e) proj e.source

theorem Pretrivialization.mk_proj_snd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : (proj x, (↑e x).snd) = ↑e x

theorem Pretrivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (proj x, (↑e x).snd) = ↑e x

def Pretrivialization.setSymm {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑e.target → Z

Composition of inverse and coercion from the subtype of the target.

theorem Pretrivialization.mem_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} : x ∈ e.target ↔ x.fst ∈ e.baseSet

theorem Pretrivialization.proj_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} (hx : x ∈ e.target) : proj (↑(LocalEquiv.symm e.toLocalEquiv) x) = x.fst

theorem Pretrivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (↑(LocalEquiv.symm e.toLocalEquiv) (b, x)) = b

theorem Pretrivialization.proj_surjOn_baseSet {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) [Nonempty F] : Set.SurjOn proj e.source e.baseSet

theorem Pretrivialization.apply_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e (↑(LocalEquiv.symm e.toLocalEquiv) x) = x

theorem Pretrivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : ↑e (↑(LocalEquiv.symm e.toLocalEquiv) (b, x)) = (b, x)

theorem Pretrivialization.symm_apply_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (hx : x ∈ e.source) : ↑(LocalEquiv.symm e.toLocalEquiv) (↑e x) = x

@[simp]

theorem Pretrivialization.symm_apply_mk_proj {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) {x : Z} (ex : x ∈ e.source) : ↑(LocalEquiv.symm e.toLocalEquiv) (proj x, (↑e x).snd) = x

@[simp]

theorem Pretrivialization.preimage_symm_proj_baseSet {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) : ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target

@[simp]

theorem Pretrivialization.preimage_symm_proj_inter {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (s : Set B) : ↑(LocalEquiv.symm e.toLocalEquiv) ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ Set.univ = (s ∩ e.baseSet) ×ˢ Set.univ

theorem Pretrivialization.target_inter_preimage_symm_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (f : Pretrivialization F proj) : f.target ∩ ↑(LocalEquiv.symm f.toLocalEquiv) ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ

theorem Pretrivialization.trans_source {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (f : Pretrivialization F proj) : (LocalEquiv.trans (LocalEquiv.symm f.toLocalEquiv) e.toLocalEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ

theorem Pretrivialization.symm_trans_symm {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) : LocalEquiv.symm (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv) = LocalEquiv.trans (LocalEquiv.symm e'.toLocalEquiv) e.toLocalEquiv

theorem Pretrivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) : (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Pretrivialization.symm_trans_target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) : (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

@[simp]

theorem Pretrivialization.coe_mem_source {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F Bundle.TotalSpace.proj) {b : B} {y : E b} : { proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet

@[simp]

theorem Pretrivialization.coe_coe_fst {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F Bundle.TotalSpace.proj) {b : B} {y : E b} (hb : b ∈ e'.baseSet) : (↑e' { proj := b, snd := y }).fst = b

theorem Pretrivialization.mk_mem_target {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] (e' : Pretrivialization F Bundle.TotalSpace.proj) {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.baseSet

theorem Pretrivialization.symm_coe_proj {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] {x : B} {y : F} (e' : Pretrivialization F Bundle.TotalSpace.proj) (h : x ∈ e'.baseSet) : (↑(LocalEquiv.symm e'.toLocalEquiv) (x, y)).proj = x

noncomputable def Pretrivialization.symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) (b : B) (y : F) : E b

A fiberwise inverse to e. This is the function F → E b that induces a local inverse B × F → TotalSpace F E of e on e.baseSet. It is defined to be 0 outside e.baseSet.

theorem Pretrivialization.symm_apply {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : Pretrivialization.symm e b y = cast (_ : E (↑(LocalEquiv.symm e.toLocalEquiv) (b, y)).proj = E b) (↑(LocalEquiv.symm e.toLocalEquiv) (b, y)).snd

theorem Pretrivialization.symm_apply_of_not_mem {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : ¬b ∈ e.baseSet) (y : F) : Pretrivialization.symm e b y = 0

theorem Pretrivialization.coe_symm_of_not_mem {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : ¬b ∈ e.baseSet) : Pretrivialization.symm e b = 0

theorem Pretrivialization.mk_symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : { proj := b, snd := Pretrivialization.symm e b y } = ↑(LocalEquiv.symm e.toLocalEquiv) (b, y)

theorem Pretrivialization.symm_proj_apply {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) (z : Bundle.TotalSpace F E) (hz : z.proj ∈ e.baseSet) : Pretrivialization.symm e z.proj (↑e z).snd = z.snd

theorem Pretrivialization.symm_apply_apply_mk {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : E b) : Pretrivialization.symm e b (↑e { proj := b, snd := y }).snd = y

theorem Pretrivialization.apply_mk_symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ↑e { proj := b, snd := Pretrivialization.symm e b y } = (b, y)

structure Trivialization {B : Type u_2} (F : Type u_3) {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] (proj : Z → B) extends LocalHomeomorph : Type (max (max u_2 u_3) u_5)

• toFun : Z → B × F
• invFun : B × F → Z
• source : Set Z
• target : Set (B × F)
• map_source' : ∀ ⦃x : Z⦄, x ∈ s.source → ↑s.toLocalEquiv x ∈ s.target
• map_target' : ∀ ⦃x : B × F⦄, x ∈ s.target → LocalEquiv.invFun s.toLocalEquiv x ∈ s.source
• left_inv' : ∀ ⦃x : Z⦄, x ∈ s.source → LocalEquiv.invFun s.toLocalEquiv (↑s.toLocalEquiv x) = x
• right_inv' : ∀ ⦃x : B × F⦄, x ∈ s.target → ↑s.toLocalEquiv (LocalEquiv.invFun s.toLocalEquiv x) = x
• open_source : IsOpen s.source
• open_target : IsOpen s.target
• continuous_toFun : ContinuousOn (↑s.toLocalEquiv) s.source
• continuous_invFun : ContinuousOn s.invFun s.target
• baseSet : Set B
• open_baseSet : IsOpen s.baseSet
• source_eq : s.source = proj ⁻¹' s.baseSet
• target_eq : s.target = s.baseSet ×ˢ Set.univ
• proj_toFun : ∀ (p : Z), p ∈ s.source → (↑s.toLocalHomeomorph p).fst = proj p

A structure extending local homeomorphisms, defining a local trivialization of a projection proj : Z → B with fiber F, as a local homeomorphism between Z and B × F defined between two sets of the form proj ⁻¹' baseSet and baseSet × F, acting trivially on the first coordinate.

theorem Trivialization.ext' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) (h₁ : e.toLocalHomeomorph = e'.toLocalHomeomorph) (h₂ : e.baseSet = e'.baseSet) : e = e'

def Trivialization.toFun' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Z → B × F

Coercion of a trivialization to a function. We don't use e.toFun in the CoeFun instance because it is actually e.toLocalEquiv.toFun, so simp will apply lemmas about toLocalEquiv. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

def Trivialization.toPretrivialization {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Pretrivialization F proj

Natural identification as a Pretrivialization.

instance Trivialization.instCoeFunTrivializationForAllProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : CoeFun (Trivialization F proj) fun x => Z → B × F

instance Trivialization.instCoeTrivializationPretrivialization {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : Coe (Trivialization F proj) (Pretrivialization F proj)

theorem Trivialization.toPretrivialization_injective {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] : Function.Injective fun e => Trivialization.toPretrivialization e

@[simp]

theorem Trivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ↑e.toLocalHomeomorph = ↑e

@[simp]

theorem Trivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : (↑e x).fst = proj x

theorem Trivialization.eqOn {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : Set.EqOn (Prod.fst ∘ ↑e) proj e.source

theorem Trivialization.mem_source {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} : x ∈ e.source ↔ proj x ∈ e.baseSet

theorem Trivialization.coe_fst' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (↑e x).fst = proj x

theorem Trivialization.mk_proj_snd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : (proj x, (↑e x).snd) = ↑e x

theorem Trivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : (proj x, (↑e x).snd) = ↑e x

theorem Trivialization.source_inter_preimage_target_inter {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set (B × F)) : e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s

@[simp]

theorem Trivialization.coe_mk {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : LocalHomeomorph Z (B × F)) (i : Set B) (j : IsOpen i) (k : e.source = proj ⁻¹' i) (l : e.target = i ×ˢ Set.univ) (m : ∀ (p : Z), p ∈ e.source → (↑e p).fst = proj p) (x : Z) : ↑{ toLocalHomeomorph := e, baseSet := i, open_baseSet := j, source_eq := k, target_eq := l, proj_toFun := m } x = ↑e x

theorem Trivialization.mem_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} : x ∈ e.target ↔ x.fst ∈ e.baseSet

theorem Trivialization.map_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x ∈ e.source

theorem Trivialization.proj_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : proj (↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) = x.fst

theorem Trivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, x)) = b

theorem Trivialization.proj_surjOn_baseSet {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) [Nonempty F] : Set.SurjOn proj e.source e.baseSet

theorem Trivialization.apply_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e (↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) = x

theorem Trivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : ↑e (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, x)) = (b, x)

@[simp]

theorem Trivialization.symm_apply_mk_proj {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (proj x, (↑e x).snd) = x

theorem Trivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) : (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Trivialization.symm_trans_target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) : (LocalEquiv.trans (LocalEquiv.symm e.toLocalEquiv) e'.toLocalEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ

theorem Trivialization.coe_fst_eventuallyEq_proj {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : Prod.fst ∘ ↑e =ᶠ[nhds x] proj

theorem Trivialization.coe_fst_eventuallyEq_proj' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x ∈ e.baseSet) : Prod.fst ∘ ↑e =ᶠ[nhds x] proj

theorem Trivialization.map_proj_nhds {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : Filter.map proj (nhds x) = nhds (proj x)

theorem Trivialization.preimage_subset_source {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : proj ⁻¹' s ⊆ e.source

theorem Trivialization.image_preimage_eq_prod_univ {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : ↑e '' (proj ⁻¹' s) = s ×ˢ Set.univ

theorem Trivialization.tendsto_nhds_iff {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {α : Type u_6} {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) : Filter.Tendsto f l (nhds z) ↔ Filter.Tendsto (proj ∘ f) l (nhds (proj z)) ∧ Filter.Tendsto (fun x => (↑e (f x)).snd) l (nhds (↑e z).snd)

theorem Trivialization.nhds_eq_inf_comap {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {z : Z} (hz : z ∈ e.source) : nhds z = Filter.comap proj (nhds (proj z)) ⊓ Filter.comap (Prod.snd ∘ ↑e) (nhds (↑e z).snd)

def Trivialization.preimageHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) : ↑(proj ⁻¹' s) ≃ₜ ↑s × F

The preimage of a subset of the base set is homeomorphic to the product with the fiber.

@[simp]

theorem Trivialization.preimageHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑(proj ⁻¹' s)) : ↑(Trivialization.preimageHomeomorph e hb) p = ({ val := proj ↑p, property := (_ : ↑p ∈ proj ⁻¹' s) }, (↑e ↑p).snd)

@[simp]

theorem Trivialization.preimageHomeomorph_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑s × F) : ↑(Homeomorph.symm (Trivialization.preimageHomeomorph e hb)) p = { val := ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (↑p.fst, p.snd), property := (_ : ↑(↑(Homeomorph.symm (Trivialization.preimageHomeomorph e hb)) p) ∈ proj ⁻¹' s) }

def Trivialization.sourceHomeomorphBaseSetProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) : ↑e.source ≃ₜ ↑e.baseSet × F

The source is homeomorphic to the product of the base set with the fiber.

@[simp]

theorem Trivialization.sourceHomeomorphBaseSetProd_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (p : ↑e.source) : ↑(Trivialization.sourceHomeomorphBaseSetProd e) p = ({ val := proj ↑p, property := (_ : proj ↑p ∈ e.baseSet) }, (↑e ↑p).snd)

@[simp]

theorem Trivialization.sourceHomeomorphBaseSetProd_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (p : ↑e.baseSet × F) : ↑(Homeomorph.symm (Trivialization.sourceHomeomorphBaseSetProd e)) p = { val := ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (↑p.fst, p.snd), property := (_ : ↑(↑(Homeomorph.symm (Trivialization.sourceHomeomorphBaseSetProd e)) p) ∈ e.source) }

def Trivialization.preimageSingletonHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) : ↑(proj ⁻¹' {b}) ≃ₜ F

Each fiber of a trivialization is homeomorphic to the specified fiber.

@[simp]

theorem Trivialization.preimageSingletonHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : ↑(proj ⁻¹' {b})) : ↑(Trivialization.preimageSingletonHomeomorph e hb) p = (↑e ↑p).snd

@[simp]

theorem Trivialization.preimageSingletonHomeomorph_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : F) : ↑(Homeomorph.symm (Trivialization.preimageSingletonHomeomorph e hb)) p = { val := ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, p), property := (_ : ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, p) ∈ proj ⁻¹' {b}) }

theorem Trivialization.continuousAt_proj {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x ∈ e.source) : ContinuousAt proj x

In the domain of a bundle trivialization, the projection is continuous

def Trivialization.compHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {Z' : Type u_6} [TopologicalSpace Z'] (h : Z' ≃ₜ Z) : Trivialization F (proj ∘ ↑h)

Composition of a Trivialization and a Homeomorph.

theorem Trivialization.continuousAt_of_comp_right {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {X : Type u_6} [TopologicalSpace X] {f : Z → X} {z : Z} (e : Trivialization F proj) (he : proj z ∈ e.baseSet) (hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)) : ContinuousAt f z

Read off the continuity of a function f : Z → X at z : Z by transferring via a trivialization of Z containing z.

theorem Trivialization.continuousAt_of_comp_left {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {X : Type u_6} [TopologicalSpace X] {f : X → Z} {x : X} (e : Trivialization F proj) (hf_proj : ContinuousAt (proj ∘ f) x) (he : proj (f x) ∈ e.baseSet) (hf : ContinuousAt (↑e ∘ f) x) : ContinuousAt f x

Read off the continuity of a function f : X → Z at x : X by transferring via a trivialization of Z containing f x.

theorem Trivialization.continuousOn {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) : ContinuousOn (↑e') e'.source

theorem Trivialization.coe_mem_source {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) {b : B} {y : E b} : { proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet

@[deprecated LocalHomeomorph.open_target]

theorem Trivialization.open_target' {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) : IsOpen e'.target

@[simp]

theorem Trivialization.coe_coe_fst {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) {b : B} {y : E b} (hb : b ∈ e'.baseSet) : (↑e' { proj := b, snd := y }).fst = b

theorem Trivialization.mk_mem_target {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) {b : B} {y : F} : (b, y) ∈ e'.target ↔ b ∈ e'.baseSet

theorem Trivialization.symm_apply_apply {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Trivialization F Bundle.TotalSpace.proj) {x : Bundle.TotalSpace F E} (hx : x ∈ e'.source) : ↑(LocalHomeomorph.symm e'.toLocalHomeomorph) (↑e' x) = x

@[simp]

theorem Trivialization.symm_coe_proj {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] {x : B} {y : F} (e : Trivialization F Bundle.TotalSpace.proj) (h : x ∈ e.baseSet) : (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (x, y)).proj = x

noncomputable def Trivialization.symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (b : B) (y : F) : E b

A fiberwise inverse to e'. The function F → E x that induces a local inverse B × F → TotalSpace F E of e' on e'.baseSet. It is defined to be 0 outside e'.baseSet.

theorem Trivialization.symm_apply {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : Trivialization.symm e b y = cast (_ : E (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y)).proj = E b) (↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y)).snd

theorem Trivialization.symm_apply_of_not_mem {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : ¬b ∈ e.baseSet) (y : F) : Trivialization.symm e b y = 0

theorem Trivialization.mk_symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : { proj := b, snd := Trivialization.symm e b y } = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) (b, y)

theorem Trivialization.symm_proj_apply {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) (z : Bundle.TotalSpace F E) (hz : z.proj ∈ e.baseSet) : Trivialization.symm e z.proj (↑e z).snd = z.snd

theorem Trivialization.symm_apply_apply_mk {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : E b) : Trivialization.symm e b (↑e { proj := b, snd := y }).snd = y

theorem Trivialization.apply_mk_symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ↑e { proj := b, snd := Trivialization.symm e b y } = (b, y)

theorem Trivialization.continuousOn_symm {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → Zero (E x)] (e : Trivialization F Bundle.TotalSpace.proj) : ContinuousOn (fun z => Bundle.TotalSpace.mk' F z.fst (Trivialization.symm e z.fst z.snd)) (e.baseSet ×ˢ Set.univ)

def Trivialization.transFiberHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {F' : Type u_6} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') : Trivialization F' proj

If e is a Trivialization of proj : Z → B with fiber F and h is a homeomorphism F ≃ₜ F', then e.trans_fiber_homeomorph h is the trivialization of proj with the fiber F' that sends p : Z to ((e p).1, h (e p).2).

@[simp]

theorem Trivialization.transFiberHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {F' : Type u_6} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') (x : Z) : ↑(Trivialization.transFiberHomeomorph e h) x = ((↑e x).fst, ↑h (↑e x).snd)

def Trivialization.coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) (b : B) (x : F) : F

Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also Trivialization.coordChangeHomeomorph for a version bundled as F ≃ₜ F.

theorem Trivialization.mk_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) : (b, Trivialization.coordChange e₁ e₂ b x) = ↑e₂ (↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x))

theorem Trivialization.coordChange_apply_snd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {p : Z} (h : proj p ∈ e₁.baseSet) : Trivialization.coordChange e₁ e₂ (proj p) (↑e₁ p).snd = (↑e₂ p).snd

theorem Trivialization.coordChange_same_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) (x : F) : Trivialization.coordChange e e b x = x

theorem Trivialization.coordChange_same {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) : Trivialization.coordChange e e b = id

theorem Trivialization.coordChange_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) (e₃ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) : Trivialization.coordChange e₂ e₃ b (Trivialization.coordChange e₁ e₂ b x) = Trivialization.coordChange e₁ e₃ b x

theorem Trivialization.continuous_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : Continuous (Trivialization.coordChange e₁ e₂ b)

def Trivialization.coordChangeHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : F ≃ₜ F

Coordinate transformation in the fiber induced by a pair of bundle trivializations, as a homeomorphism.

@[simp]

theorem Trivialization.coordChangeHomeomorph_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) : ↑(Trivialization.coordChangeHomeomorph e₁ e₂ h₁ h₂) = Trivialization.coordChange e₁ e₂ b

theorem Trivialization.isImage_preimage_prod {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) : LocalHomeomorph.IsImage e.toLocalHomeomorph (proj ⁻¹' s) (s ×ˢ Set.univ)

def Trivialization.restrOpen {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) (hs : IsOpen s) : Trivialization F proj

Restrict a Trivialization to an open set in the base.

theorem Trivialization.frontier_preimage {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) : e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)

noncomputable def Trivialization.piecewise {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) (s : Set B) (Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))) : Trivialization F proj

Given two bundle trivializations e, e' of proj : Z → B and a set s : Set B such that the base sets of e and e' intersect frontier s on the same set and e p = e' p whenever proj p ∈ e.baseSet ∩ frontier s, e.piecewise e' s Hs Heq is the bundle trivialization over Set.ite s e.baseSet e'.baseSet that is equal to e on proj ⁻¹ s and is equal to e' otherwise.

noncomputable def Trivialization.piecewiseLeOfEq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] [LinearOrder B] [OrderTopology B] (e : Trivialization F proj) (e' : Trivialization F proj) (a : B) (He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) (Heq : ∀ (p : Z), proj p = a → ↑e p = ↑e' p) : Trivialization F proj

Given two bundle trivializations e, e' of a topological fiber bundle proj : Z → B over a linearly ordered base B and a point a ∈ e.baseSet ∩ e'.baseSet such that e equals e' on proj ⁻¹' {a}, e.piecewise_le_of_eq e' a He He' Heq is the bundle trivialization over Set.ite (Iic a) e.baseSet e'.baseSet that is equal to e on points p such that proj p ≤ a and is equal to e' otherwise.

noncomputable def Trivialization.piecewiseLe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] [LinearOrder B] [OrderTopology B] (e : Trivialization F proj) (e' : Trivialization F proj) (a : B) (He : a ∈ e.baseSet) (He' : a ∈ e'.baseSet) : Trivialization F proj

Given two bundle trivializations e, e' of a topological fiber bundle proj : Z → B over a linearly ordered base B and a point a ∈ e.baseSet ∩ e'.baseSet, e.piecewise_le e' a He He' is the bundle trivialization over Set.ite (Iic a) e.baseSet e'.baseSet that is equal to e on points p such that proj p ≤ a and is equal to ((e' p).1, h (e' p).2) otherwise, where h = e'.coord_change_homeomorph e _ _ is the homeomorphism of the fiber such that h (e' p).2 = (e p).2 whenever e p = a.

noncomputable def Trivialization.disjointUnion {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) (H : Disjoint e.baseSet e'.baseSet) : Trivialization F proj

Given two bundle trivializations e, e' over disjoint sets, e.disjoint_union e' H is the bundle trivialization over the union of the base sets that agrees with e and e' over their base sets.