Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-24 07:49 3590dc29

View on Github →

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.

Estimated changes

deleted theorem analytic_at.continuous_at