Theorems · Theorem · algebraic topology

Bundle.Pretrivialization.toPartialEquiv_injective

∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [Nonempty F], Function.Injective Bundle.Pretrivialization.toPartialEquiv

If the fiber is nonempty, then the projection also is.

Defined in: Mathlib.Topology.FiberBundle.Trivialization
Cited by: 0 results in Mathlib
Foundations: Depth 70 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.

Cites10

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.imageproof · cited by 5,609
PartialEquiv.targetproof · cited by 650
PartialEquivstatement and proof · cited by 335
Bundle.Pretrivializationstatement and proof · cited by 111
Bundle.Pretrivialization.baseSetproof · cited by 80
Bundle.Pretrivialization.toPartialEquivstatement and proof · cited by 77
Set.fst_image_prodproof · cited by 8
Bundle.Pretrivialization.target_eqproof · cited by 4
Bundle.Pretrivialization.ext'proof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.