Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-26 16:01 178a3265

View on Github →

chore(topology/category/Top/limits): split file (#18871) Per https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233487.20last.20minute.20split.3F This file is already being ported at https://github.com/leanprover-community/mathlib4/pull/3487, but:

  • it's not going so well right now
  • it is going well up to the point of the proposed new limits/basic.lean
  • that is sufficient to port the files needed for Copenhagen

Estimated changes

deleted def Top.binary_cofan
deleted def Top.colimit_cocone
deleted theorem Top.colimit_is_open_iff
deleted theorem Top.colimit_topology
deleted theorem Top.embedding_prod_map
deleted theorem Top.induced_of_is_limit
deleted theorem Top.inducing_prod_map
deleted def Top.limit_cone
deleted def Top.limit_cone_infi
deleted theorem Top.limit_topology
deleted def Top.pi_fan
deleted def Top.pi_fan_is_limit
deleted def Top.pi_iso_pi
deleted theorem Top.pi_iso_pi_hom_apply
deleted theorem Top.pi_iso_pi_inv_π
deleted def Top.pi_π
deleted def Top.prod_binary_fan
deleted def Top.prod_fst
deleted def Top.prod_iso_prod
deleted theorem Top.prod_iso_prod_hom_fst
deleted theorem Top.prod_iso_prod_hom_snd
deleted theorem Top.prod_iso_prod_inv_fst
deleted theorem Top.prod_iso_prod_inv_snd
deleted def Top.prod_snd
deleted theorem Top.prod_topology
deleted def Top.pullback_cone
deleted def Top.pullback_fst
deleted theorem Top.pullback_fst_range
deleted def Top.pullback_snd
deleted theorem Top.pullback_snd_range
deleted theorem Top.pullback_topology
deleted theorem Top.range_prod_map
deleted theorem Top.range_pullback_map
deleted def Top.sigma_cofan
deleted def Top.sigma_iso_sigma
deleted def Top.sigma_ι
added def Top.limit_cone
added def Top.binary_cofan
added theorem Top.embedding_prod_map
added theorem Top.inducing_prod_map
added theorem Top.limit_topology
added def Top.pi_fan
added def Top.pi_iso_pi
added theorem Top.pi_iso_pi_inv_π
added def Top.pi_π
added def Top.prod_fst
added def Top.prod_snd
added theorem Top.prod_topology
added theorem Top.range_prod_map
added def Top.sigma_cofan
added def Top.sigma_ι
added theorem Top.colimit_topology
added def Top.pullback_fst
added theorem Top.pullback_fst_range
added def Top.pullback_snd
added theorem Top.pullback_snd_range
added theorem Top.pullback_topology
added theorem Top.range_pullback_map