Mathlib Map

Theorems · Definition · category theory

TopPair

Type (u_1 + 1)

A pair of topological spaces consists of an embedding f : A ⟶ X in TopCat.

Defined in
Mathlib.Topology.Category.TopPair
Cited by
67 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TopPair.HomologyPretheory.Hₚ · cited by 32HomologyPretheory.HₚTopPair.incl · cited by 28TopPair.inclTopPair.HomologyPretheory.Hom.homₚ · cited by 22Hom.homₚTopPair.fst · cited by 21TopPair.fstTopPair.snd · cited by 21TopPair.sndTopPair.HomologyPretheory.iso · cited by 21HomologyPretheory.isoTopPair.Homotopy · cited by 19TopPair.HomotopyTopPair.Hom.fst · cited by 16Hom.fstTopPair.Hom.snd · cited by 16Hom.sndTopPair.proj₂ · cited by 15TopPair.proj₂TopPair.map · cited by 14TopPair.mapTopPair.HomologyPretheory.δ · cited by 12HomologyPretheory.δTopPair.Homotopy.fst · cited by 12Homotopy.fstTopPair.Homotopy.snd · cited by 12Homotopy.sndTopPair.ofTopCat · cited by 8TopPair.ofTopCatTop.top · cited by 9680Top.topTopCat.isEmbedding · cited by 67TopCat.isEmbeddingCategoryTheory.MorphismProperty.Arrow · cited by 17MorphismProperty.ArrowTopPairCITED BYCITES

Cites3

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

Cited by112

Results whose statement or proof uses this declaration.