Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 05:50 d38aca11

View on Github →

chore(topology/*): Use finite in place of fintype where possible (#15891) Satisfy the fintype_finite linter.

Estimated changes

modified theorem infi_supr_of_antitone
modified theorem infi_supr_of_monotone
modified theorem set.Inter_Union_of_antitone
modified theorem set.Inter_Union_of_monotone
modified theorem set.Union_Inter_of_antitone
modified theorem set.Union_Inter_of_monotone
modified theorem set.finite.pi
modified theorem supr_infi_of_antitone
modified theorem supr_infi_of_monotone
modified theorem filter.Inter_mem
modified theorem filter.eventually_all
added theorem filter.infi_principal
modified theorem filter.Coprod_cofinite
added theorem closure_Union
deleted theorem closure_Union_of_fintype
added theorem interior_Inter
deleted theorem interior_Inter_of_fintype
modified theorem is_closed_Union
modified theorem is_open_Inter
modified theorem bornology.is_bounded_Union
modified theorem nhds_within_pi_univ_eq
modified theorem compact_Union
modified theorem is_clopen_Inter
modified theorem is_clopen_Union