Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 03:30 e1c8bded

View on Github →

feat(topology/support): add lemmas, fix a name (#15484)

  • generalize support_smul_subset_left to smul_with_zero;
  • add tsupport_smul_subset_left;
  • rename not_mem_closure_mul_support_iff_eventually_eq to not_mem_mul_tsupport_iff_eventually_eq;
  • add continuous_of_mul_tsupport.

Estimated changes