Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-23 17:55 b7f03239

View on Github →

feat(topology): interior of a finite product of sets (#8695) Also finishes the filter inf work from #8657 proving stronger lemmas for filter.infi

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.Inter_dite

added theorem set.Inter_ite

added theorem set.Union_dite

added theorem set.Union_ite

added theorem set.image_projection_prod

Modified src/measure_theory/measurable_space.lean

Modified src/order/complete_lattice.lean

added theorem infi_dite

added theorem infi_ite

added theorem supr_dite

added theorem supr_ite

Modified src/order/filter/at_top_bot.lean

Modified src/order/filter/basic.lean

added theorem filter.exists_Inter_of_mem_infi

added theorem filter.mem_infi_of_Inter

added theorem filter.mem_infi_of_fintype

Modified src/topology/bases.lean

Modified src/topology/constructions.lean

added theorem interior_pi_set

added theorem mem_nhds_pi

added theorem set_pi_mem_nhds_iff

Modified src/topology/continuous_on.lean