Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-23 08:40 421ed703

View on Github →

chore(topology/metric_space/baire): review (#3146)

  • Simplify some proofs in topology/metric_space/baire;
  • Allow dependency on hi : i ∈ S in some bUnion/bInter lemmas.

Estimated changes

added theorem set.eq_univ_of_subset
modified theorem set.countable.bUnion
modified theorem set.bInter_eq_Inter
modified theorem set.bUnion_eq_Union
modified theorem set.sInter_bUnion
modified theorem set.sInter_eq_Inter
modified theorem set.sInter_range
modified theorem set.sUnion_bUnion
modified theorem set.sUnion_eq_Union
modified theorem set.sUnion_range
modified theorem dense_bInter_of_Gδ
added theorem dense_inter_of_Gδ
added theorem is_Gδ.inter
added theorem is_Gδ_Inter
modified theorem is_Gδ_Inter_of_open
added theorem is_Gδ_bInter
modified theorem is_Gδ_bInter_of_open
added theorem is_Gδ_univ