Theorems · Theorem · algebraic topology

FiberPrebundle.isOpen_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)
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj), IsOpen e.source

Defined in: Mathlib.Topology.FiberBundle.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites23

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

TopologicalSpacestatement and proof · cited by 24,529
Set.Elemproof · cited by 7,166
IsOpenstatement · cited by 2,400
Set.extproof · cited by 2,266
PartialEquiv.sourcestatement · cited by 964
PartialEquiv.toFunproof · cited by 821
Bundle.TotalSpacestatement and proof · cited by 766
PartialEquiv.targetproof · cited by 650
PartialEquiv.symmproof · cited by 453
Bundle.TotalSpace.projstatement and proof · cited by 447
Bundle.Pretrivializationstatement and proof · cited by 111
Bundle.Pretrivialization.baseSetproof · cited by 80

Cited by2

Results whose statement or proof uses this declaration.

FiberPrebundle.trivializationOfMemPretrivializationAtlasproof · cited by 5
FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_interproof · cited by 0