Theorems · Theorem · algebraic topology

FiberPrebundle.mem_pretrivializationAt_source

∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B) (x : E b),
  ⟨b, x⟩ ∈ (a.pretrivializationAt b).source

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace