Theorems · Theorem · algebraic topology

Bundle.Trivial.eq_trivialization

∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [i : MemTrivializationAtlas e],
  e = Bundle.Trivial.trivialization B F

Defined in

Mathlib.Topology.FiberBundle.Constructions

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMemTrivializationAtlas