Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-20 14:59 b7cc093e

View on Github →

chore(topology/constructions): use variables (#16562) Also move continuous_pi_iff up and golf its proof.

Estimated changes

Modified src/topology/constructions.lean

modified theorem continuous.update

modified theorem continuous_apply

modified theorem continuous_apply_apply

modified theorem continuous_at.update

modified theorem continuous_at_apply

modified theorem continuous_at_pi

modified theorem continuous_pi

modified theorem continuous_pi_iff

modified theorem continuous_update

modified theorem exists_finset_piecewise_mem_of_mem_nhds

modified theorem filter.tendsto.apply

modified theorem filter.tendsto.update

modified theorem inducing_infi_to_pi

modified theorem interior_pi_set

modified theorem is_closed_set_pi

modified theorem is_open_set_pi

modified theorem mem_nhds_of_pi_mem_nhds

modified theorem nhds_pi

modified theorem pi_eq_generate_from

modified theorem pi_generate_from_eq

modified theorem pi_generate_from_eq_finite

modified theorem set_pi_mem_nhds

modified theorem set_pi_mem_nhds_iff

modified theorem tendsto_pi_nhds