mathlib3
3590dc29 - feat(topology/uniform_space/uniform_convergence): slightly generalize theorems (#10444)

Commit
4 years ago
feat(topology/uniform_space/uniform_convergence): slightly generalize theorems (#10444) * add `protected` to some theorems; * assume `∀ᶠ n, continuous (F n)` instead of `∀ n, continuous (F n)`; * get rid of `F n` in lemmas like `continuous_within_at_of_locally_uniform_approx_of_continuous_within_at`; instead, assume that there exists a continuous `F` that approximates `f`.
Author
Parents
Loading