Documentation

Mathlib.Topology.FiberBundle.Trivialization

Trivializations #

Main definitions #

Basic definitions #

Operations on bundles #

We provide the following operations on Trivializations.

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 : ZB) extends PartialEquiv :
Type (max (max u_2 u_3) u_5)

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.

  • toFun : ZB × F
  • invFun : B × FZ
  • source : Set Z
  • target : Set (B × F)
  • map_source' : ∀ ⦃x : Z⦄, x self.sourceself.toPartialEquiv x self.target
  • map_target' : ∀ ⦃x : B × F⦄, x self.targetself.invFun x self.source
  • left_inv' : ∀ ⦃x : Z⦄, x self.sourceself.invFun (self.toPartialEquiv x) = x
  • right_inv' : ∀ ⦃x : B × F⦄, x self.targetself.toPartialEquiv (self.invFun x) = x
  • open_target : IsOpen self.target
  • baseSet : Set B
  • open_baseSet : IsOpen self.baseSet
  • source_eq : self.source = proj ⁻¹' self.baseSet
  • target_eq : self.target = self.baseSet ×ˢ Set.univ
  • proj_toFun : pself.source, (self.toPartialEquiv p).1 = proj p
Instances For
    theorem Pretrivialization.open_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (self : Pretrivialization F proj) :
    IsOpen self.target
    theorem Pretrivialization.open_baseSet {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (self : Pretrivialization F proj) :
    IsOpen self.baseSet
    theorem Pretrivialization.source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (self : Pretrivialization F proj) :
    self.source = proj ⁻¹' self.baseSet
    theorem Pretrivialization.target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (self : Pretrivialization F proj) :
    self.target = self.baseSet ×ˢ Set.univ
    theorem Pretrivialization.proj_toFun {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (self : Pretrivialization F proj) (p : Z) :
    p self.source(self.toPartialEquiv p).1 = proj p
    def Pretrivialization.toFun' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) :
    ZB × F

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

    Equations
    • e = e.toPartialEquiv
    Instances For
      instance Pretrivialization.instCoeFunForallProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} :
      CoeFun (Pretrivialization F proj) fun (x : Pretrivialization F proj) => ZB × F
      Equations
      • Pretrivialization.instCoeFunForallProd = { coe := Pretrivialization.toFun' }
      theorem Pretrivialization.ext' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) (h₁ : e.toPartialEquiv = e'.toPartialEquiv) (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 : ZB} {e : Pretrivialization F proj} {e' : Pretrivialization F proj} (h₁ : ∀ (x : Z), e x = e' x) (h₂ : ∀ (x : B × F), e.symm x = e'.symm x) (h₃ : e.baseSet = e'.baseSet) :
      e = e'
      theorem Pretrivialization.toPartialEquiv_injective {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [Nonempty F] :
      Function.Injective Pretrivialization.toPartialEquiv

      If the fiber is nonempty, then the projection also is.

      @[simp]
      theorem Pretrivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) :
      e.toPartialEquiv = e
      @[simp]
      theorem Pretrivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {x : Z} (ex : x e.source) :
      (e x).1 = proj x
      theorem Pretrivialization.mem_source {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (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 : ZB} (e : Pretrivialization F proj) {x : Z} (ex : proj x e.baseSet) :
      (e x).1 = proj x
      theorem Pretrivialization.eqOn {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (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 : ZB} (e : Pretrivialization F proj) {x : Z} (ex : x e.source) :
      (proj x, (e x).2) = e x
      theorem Pretrivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {x : Z} (ex : proj x e.baseSet) :
      (proj x, (e x).2) = e x
      def Pretrivialization.setSymm {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) :
      e.targetZ

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

      Equations
      • e.setSymm = e.target.restrict e.symm
      Instances For
        theorem Pretrivialization.mem_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {x : B × F} :
        x e.target x.1 e.baseSet
        theorem Pretrivialization.proj_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {x : B × F} (hx : x e.target) :
        proj (e.symm x) = x.1
        theorem Pretrivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b e.baseSet) :
        proj (e.symm (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 : ZB} (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 : ZB} (e : Pretrivialization F proj) {x : B × F} (hx : x e.target) :
        e (e.symm x) = x
        theorem Pretrivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) {b : B} {x : F} (hx : b e.baseSet) :
        e (e.symm (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 : ZB} (e : Pretrivialization F proj) {x : Z} (hx : x e.source) :
        e.symm (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 : ZB} (e : Pretrivialization F proj) {x : Z} (ex : x e.source) :
        e.symm (proj x, (e x).2) = 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 : ZB} (e : Pretrivialization F proj) :
        e.symm ⁻¹' (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 : ZB} (e : Pretrivialization F proj) (s : Set B) :
        e.symm ⁻¹' (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 : ZB} (e : Pretrivialization F proj) (f : Pretrivialization F proj) :
        f.target f.symm ⁻¹' 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 : ZB} (e : Pretrivialization F proj) (f : Pretrivialization F proj) :
        (f.symm.trans e.toPartialEquiv).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 : ZB} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) :
        (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv
        theorem Pretrivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) :
        (e.symm.trans e'.toPartialEquiv).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 : ZB} (e : Pretrivialization F proj) (e' : Pretrivialization F proj) :
        (e.symm.trans e'.toPartialEquiv).target = (e.baseSet e'.baseSet) ×ˢ Set.univ
        @[simp]
        theorem Pretrivialization.coe_mem_source {B : Type u_2} {F : Type u_3} {E : BType 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 : BType 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 }).1 = b
        theorem Pretrivialization.mk_mem_target {B : Type u_2} {F : Type u_3} {E : BType 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 : BType u_4} [TopologicalSpace B] [TopologicalSpace F] {x : B} {y : F} (e' : Pretrivialization F Bundle.TotalSpace.proj) (h : x e'.baseSet) :
        (e'.symm (x, y)).proj = x
        noncomputable def Pretrivialization.symm {B : Type u_2} {F : Type u_3} {E : BType 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.

        Equations
        • e.symm b y = if hb : b e.baseSet then cast (e.symm (b, y)).snd else 0
        Instances For
          theorem Pretrivialization.symm_apply {B : Type u_2} {F : Type u_3} {E : BType 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.symm b y = cast (e.symm (b, y)).snd
          theorem Pretrivialization.symm_apply_of_not_mem {B : Type u_2} {F : Type u_3} {E : BType u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : be.baseSet) (y : F) :
          e.symm b y = 0
          theorem Pretrivialization.coe_symm_of_not_mem {B : Type u_2} {F : Type u_3} {E : BType u_4} [TopologicalSpace B] [TopologicalSpace F] [(x : B) → Zero (E x)] (e : Pretrivialization F Bundle.TotalSpace.proj) {b : B} (hb : be.baseSet) :
          e.symm b = 0
          theorem Pretrivialization.mk_symm {B : Type u_2} {F : Type u_3} {E : BType 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 := e.symm b y } = e.symm (b, y)
          theorem Pretrivialization.symm_proj_apply {B : Type u_2} {F : Type u_3} {E : BType 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) :
          e.symm z.proj (e z).2 = z.snd
          theorem Pretrivialization.symm_apply_apply_mk {B : Type u_2} {F : Type u_3} {E : BType 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) :
          e.symm b (e { proj := b, snd := y }).2 = y
          theorem Pretrivialization.apply_mk_symm {B : Type u_2} {F : Type u_3} {E : BType 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 := e.symm 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 : ZB) extends PartialHomeomorph :
          Type (max (max u_2 u_3) u_5)

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

          • toFun : ZB × F
          • invFun : B × FZ
          • source : Set Z
          • target : Set (B × F)
          • map_source' : ∀ ⦃x : Z⦄, x self.sourceself.toPartialEquiv x self.target
          • map_target' : ∀ ⦃x : B × F⦄, x self.targetself.invFun x self.source
          • left_inv' : ∀ ⦃x : Z⦄, x self.sourceself.invFun (self.toPartialEquiv x) = x
          • right_inv' : ∀ ⦃x : B × F⦄, x self.targetself.toPartialEquiv (self.invFun x) = x
          • open_source : IsOpen self.source
          • open_target : IsOpen self.target
          • continuousOn_toFun : ContinuousOn (self.toPartialEquiv) self.source
          • continuousOn_invFun : ContinuousOn self.invFun self.target
          • baseSet : Set B
          • open_baseSet : IsOpen self.baseSet
          • source_eq : self.source = proj ⁻¹' self.baseSet
          • target_eq : self.target = self.baseSet ×ˢ Set.univ
          • proj_toFun : pself.source, (self.toPartialHomeomorph p).1 = proj p
          Instances For
            theorem Trivialization.open_baseSet {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : ZB} (self : Trivialization F proj) :
            IsOpen self.baseSet
            theorem Trivialization.source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : ZB} (self : Trivialization F proj) :
            self.source = proj ⁻¹' self.baseSet
            theorem Trivialization.target_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : ZB} (self : Trivialization F proj) :
            self.target = self.baseSet ×ˢ Set.univ
            theorem Trivialization.proj_toFun {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : ZB} (self : Trivialization F proj) (p : Z) :
            p self.source(self.toPartialHomeomorph p).1 = proj p
            theorem Trivialization.ext' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) (h₁ : e.toPartialHomeomorph = e'.toPartialHomeomorph) (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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) :
            ZB × F

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

            Equations
            • e = e.toPartialEquiv
            Instances For
              def Trivialization.toPretrivialization {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) :

              Natural identification as a Pretrivialization.

              Equations
              • e.toPretrivialization = { toPartialEquiv := e.toPartialEquiv, open_target := , baseSet := e.baseSet, open_baseSet := , source_eq := , target_eq := , proj_toFun := }
              Instances For
                instance Trivialization.instCoeFunForallProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] :
                CoeFun (Trivialization F proj) fun (x : Trivialization F proj) => ZB × F
                Equations
                • Trivialization.instCoeFunForallProd = { coe := Trivialization.toFun' }
                instance Trivialization.instCoePretrivialization {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] :
                Equations
                • Trivialization.instCoePretrivialization = { coe := Trivialization.toPretrivialization }
                theorem Trivialization.toPretrivialization_injective {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] :
                Function.Injective fun (e : Trivialization F proj) => e.toPretrivialization
                @[simp]
                theorem Trivialization.coe_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) :
                e.toPartialHomeomorph = e
                @[simp]
                theorem Trivialization.coe_fst {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x e.source) :
                (e x).1 = proj x
                theorem Trivialization.eqOn {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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 : ZB} [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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x e.baseSet) :
                (e x).1 = proj x
                theorem Trivialization.mk_proj_snd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x e.source) :
                (proj x, (e x).2) = e x
                theorem Trivialization.mk_proj_snd' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : proj x e.baseSet) :
                (proj x, (e x).2) = 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 : ZB} [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 : ZB} [TopologicalSpace Z] (e : PartialHomeomorph Z (B × F)) (i : Set B) (j : IsOpen i) (k : e.source = proj ⁻¹' i) (l : e.target = i ×ˢ Set.univ) (m : pe.source, (e p).1 = proj p) (x : Z) :
                { toPartialHomeomorph := 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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} :
                x e.target x.1 e.baseSet
                theorem Trivialization.map_target {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x e.target) :
                e.symm 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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x e.target) :
                proj (e.symm x) = x.1
                theorem Trivialization.proj_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b e.baseSet) :
                proj (e.symm (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 : ZB} [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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : B × F} (hx : x e.target) :
                e (e.symm x) = x
                theorem Trivialization.apply_symm_apply' {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} {x : F} (hx : b e.baseSet) :
                e (e.symm (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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x e.source) :
                e.symm (proj x, (e x).2) = x
                theorem Trivialization.symm_trans_source_eq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) :
                (e.symm.trans e'.toPartialEquiv).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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) :
                (e.symm.trans e'.toPartialEquiv).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 : ZB} [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 : ZB} [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 : ZB} [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 : ZB} [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 : ZB} [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 : ZB} [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)).2) l (nhds (e z).2)
                theorem Trivialization.nhds_eq_inf_comap {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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).2)
                def Trivialization.preimageHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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.

                Equations
                Instances For
                  @[simp]
                  theorem Trivialization.preimageHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s e.baseSet) (p : (proj ⁻¹' s)) :
                  (e.preimageHomeomorph hb) p = (proj p, , (e p).2)
                  @[simp]
                  theorem Trivialization.preimageHomeomorph_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {s : Set B} (hb : s e.baseSet) (p : s × F) :
                  (e.preimageHomeomorph hb).symm p = e.symm (p.1, p.2),
                  def Trivialization.sourceHomeomorphBaseSetProd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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.

                  Equations
                  Instances For
                    @[simp]
                    theorem Trivialization.sourceHomeomorphBaseSetProd_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (p : e.source) :
                    e.sourceHomeomorphBaseSetProd p = (proj p, , (e p).2)
                    @[simp]
                    theorem Trivialization.sourceHomeomorphBaseSetProd_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (p : e.baseSet × F) :
                    e.sourceHomeomorphBaseSetProd.symm p = e.symm (p.1, p.2),
                    def Trivialization.preimageSingletonHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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.

                    Equations
                    Instances For
                      @[simp]
                      theorem Trivialization.preimageSingletonHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b e.baseSet) (p : (proj ⁻¹' {b})) :
                      (e.preimageSingletonHomeomorph hb) p = (e p).2
                      @[simp]
                      theorem Trivialization.preimageSingletonHomeomorph_symm_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (hb : b e.baseSet) (p : F) :
                      (e.preimageSingletonHomeomorph hb).symm p = e.symm (b, p),
                      theorem Trivialization.continuousAt_proj {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {x : Z} (ex : x e.source) :

                      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 : ZB} [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.

                      Equations
                      • e.compHomeomorph h = { toPartialHomeomorph := h.toPartialHomeomorph.trans e.toPartialHomeomorph, baseSet := e.baseSet, open_baseSet := , source_eq := , target_eq := , proj_toFun := }
                      Instances For
                        theorem Trivialization.continuousAt_of_comp_right {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] {X : Type u_6} [TopologicalSpace X] {f : ZX} {z : Z} (e : Trivialization F proj) (he : proj z e.baseSet) (hf : ContinuousAt (f e.symm) (e 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 : ZB} [TopologicalSpace Z] {X : Type u_6} [TopologicalSpace X] {f : XZ} {x : X} (e : Trivialization F proj) (hf_proj : ContinuousAt (proj f) x) (he : proj (f x) e.baseSet) (hf : ContinuousAt (e 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 : BType 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 : BType 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 PartialHomeomorph.open_target]
                        theorem Trivialization.open_target' {B : Type u_2} {F : Type u_3} {E : BType 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 : BType 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 }).1 = b
                        theorem Trivialization.mk_mem_target {B : Type u_2} {F : Type u_3} {E : BType 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 : BType 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) :
                        e'.symm (e' x) = x
                        @[simp]
                        theorem Trivialization.symm_coe_proj {B : Type u_2} {F : Type u_3} {E : BType 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) :
                        (e.symm (x, y)).proj = x
                        noncomputable def Trivialization.symm {B : Type u_2} {F : Type u_3} {E : BType 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.

                        Equations
                        • e.symm b y = e.toPretrivialization.symm b y
                        Instances For
                          theorem Trivialization.symm_apply {B : Type u_2} {F : Type u_3} {E : BType 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.symm b y = cast (e.symm (b, y)).snd
                          theorem Trivialization.symm_apply_of_not_mem {B : Type u_2} {F : Type u_3} {E : BType 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 : be.baseSet) (y : F) :
                          e.symm b y = 0
                          theorem Trivialization.mk_symm {B : Type u_2} {F : Type u_3} {E : BType 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 := e.symm b y } = e.symm (b, y)
                          theorem Trivialization.symm_proj_apply {B : Type u_2} {F : Type u_3} {E : BType 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) :
                          e.symm z.proj (e z).2 = z.snd
                          theorem Trivialization.symm_apply_apply_mk {B : Type u_2} {F : Type u_3} {E : BType 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) :
                          e.symm b (e { proj := b, snd := y }).2 = y
                          theorem Trivialization.apply_mk_symm {B : Type u_2} {F : Type u_3} {E : BType 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 := e.symm b y } = (b, y)
                          theorem Trivialization.continuousOn_symm {B : Type u_2} {F : Type u_3} {E : BType 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 : B × F) => Bundle.TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ Set.univ)
                          def Trivialization.transFiberHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] {F' : Type u_6} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') :

                          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).

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem Trivialization.transFiberHomeomorph_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] {F' : Type u_6} [TopologicalSpace F'] (e : Trivialization F proj) (h : F ≃ₜ F') (x : Z) :
                            (e.transFiberHomeomorph h) x = ((e x).1, h (e x).2)
                            def Trivialization.coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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.

                            Equations
                            • e₁.coordChange e₂ b x = (e₂ (e₁.symm (b, x))).2
                            Instances For
                              theorem Trivialization.mk_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b e₁.baseSet) (h₂ : b e₂.baseSet) (x : F) :
                              (b, e₁.coordChange e₂ b x) = e₂ (e₁.symm (b, x))
                              theorem Trivialization.coordChange_apply_snd {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {p : Z} (h : proj p e₁.baseSet) :
                              e₁.coordChange e₂ (proj p) (e₁ p).2 = (e₂ p).2
                              theorem Trivialization.coordChange_same_apply {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b e.baseSet) (x : F) :
                              e.coordChange 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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) {b : B} (h : b e.baseSet) :
                              e.coordChange e b = id
                              theorem Trivialization.coordChange_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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) :
                              e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x
                              theorem Trivialization.continuous_coordChange {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b e₁.baseSet) (h₂ : b e₂.baseSet) :
                              Continuous (e₁.coordChange e₂ b)
                              def Trivialization.coordChangeHomeomorph {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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.

                              Equations
                              • e₁.coordChangeHomeomorph e₂ h₁ h₂ = { toFun := e₁.coordChange e₂ b, invFun := e₂.coordChange e₁ b, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
                              Instances For
                                @[simp]
                                theorem Trivialization.coordChangeHomeomorph_coe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e₁ : Trivialization F proj) (e₂ : Trivialization F proj) {b : B} (h₁ : b e₁.baseSet) (h₂ : b e₂.baseSet) :
                                (e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b
                                theorem Trivialization.isImage_preimage_prod {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) :
                                e.IsImage (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 : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (s : Set B) (hs : IsOpen s) :

                                Restrict a Trivialization to an open set in the base.

                                Equations
                                • e.restrOpen s hs = { toPartialHomeomorph := (.restr ).symm, baseSet := e.baseSet s, open_baseSet := , source_eq := , target_eq := , proj_toFun := }
                                Instances For
                                  theorem Trivialization.frontier_preimage {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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 : ZB} [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))) :

                                  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.baseSetfrontier 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.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def Trivialization.piecewiseLeOfEq {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [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 = ae p = e' p) :

                                    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.

                                    Equations
                                    • e.piecewiseLeOfEq e' a He He' Heq = e.piecewise e' (Set.Iic a)
                                    Instances For
                                      noncomputable def Trivialization.piecewiseLe {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] [LinearOrder B] [OrderTopology B] (e : Trivialization F proj) (e' : Trivialization F proj) (a : B) (He : a e.baseSet) (He' : a e'.baseSet) :

                                      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.

                                      Equations
                                      • e.piecewiseLe e' a He He' = e.piecewiseLeOfEq (e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) a He He'
                                      Instances For
                                        noncomputable def Trivialization.disjointUnion {B : Type u_2} {F : Type u_3} {Z : Type u_5} [TopologicalSpace B] [TopologicalSpace F] {proj : ZB} [TopologicalSpace Z] (e : Trivialization F proj) (e' : Trivialization F proj) (H : Disjoint e.baseSet e'.baseSet) :

                                        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.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For