Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-21 08:15 d2057271

View on Github →

feat(topology/constructions): add/golf lemmas about sigma (#16571)

  • add some iff lemmas;
  • golf some proofs.

Estimated changes

added theorem comap_sigma_mk_nhds
added theorem continuous.sigma_map
modified theorem continuous_sigma
added theorem continuous_sigma_iff
modified theorem continuous_sigma_map
modified theorem embedding_sigma_map
added theorem inducing_sigma_map
deleted theorem is_closed_sigma_mk
modified theorem is_open_map_sigma
added theorem is_open_map_sigma_map
added theorem sigma.nhds_eq
added theorem sigma.nhds_mk