Theorems · Theorem · algebraic topology

Bundle.Pretrivialization.coe_coe_fst

∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B} {y : E b}, b ∈ e'.baseSet → (↑e' ⟨b, y⟩).1 = b

Defined in: Mathlib.Topology.FiberBundle.Trivialization
Cited by: 0 results in Mathlib
Foundations: Depth 9 from the axioms · uses propext
Assumes: TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
Bundle.TotalSpacestatement · cited by 766
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.toFun'statement · cited by 53
Bundle.Pretrivialization.coe_fstproof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.