Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eventually_singleton_add_smul_subset

Modification history

2021-12-23 02:02
src/analysis/normed_space/pointwise.lean
feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820) …
Added eventually_singleton_add_smul_subsetView on Github →