Theorems · Theorem · algebraic topology

Bundle.Pretrivialization.symm_proj_apply

∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (z : Bundle.TotalSpace F E), z.proj ∈ e.baseSet → e.symm z.proj (↑e z).2 = z.snd

Defined in: Mathlib.Topology.FiberBundle.Trivialization
Cited by: 2 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
PartialEquiv.toFunproof · cited by 821
Bundle.TotalSpacestatement and proof · cited by 766
PartialEquiv.symmproof · cited by 453
Bundle.TotalSpace.projstatement and proof · cited by 447
Bundle.Pretrivializationstatement and proof · cited by 111
Bundle.Pretrivialization.baseSetstatement and proof · cited by 80
Bundle.Pretrivialization.toPartialEquivproof · cited by 77
Bundle.TotalSpace.sndstatement and proof · cited by 76
Bundle.Pretrivialization.toFun'statement and proof · cited by 53
Bundle.Pretrivialization.symmstatement · cited by 26

Cited by2

Results whose statement or proof uses this declaration.

Bundle.Trivialization.symm_proj_applyproof · cited by 1
Bundle.Pretrivialization.symm_apply_apply_mkproof · cited by 1