Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-19 09:58 3d948bf1

View on Github →

feat(analysis/normed_space): interior of closed_ball etc (#2723)

define sphere x r
prove formulas for interior, closure, and frontier of open and closed balls in real normed vector spaces.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem closure_ball

added theorem frontier_ball

added theorem frontier_closed_ball'

added theorem frontier_closed_ball

added theorem interior_closed_ball'

added theorem interior_closed_ball

modified theorem submodule.eq_top_of_nonempty_interior

Modified src/topology/basic.lean

added theorem preimage_interior_subset_interior_preimage

Modified src/topology/continuous_on.lean

Modified src/topology/metric_space/basic.lean

modified theorem metric.ball_eq_empty_iff_nonpos

added theorem metric.ball_subset_interior_closed_ball

added theorem metric.ball_union_sphere

added theorem metric.closed_ball_diff_ball

added theorem metric.closed_ball_diff_sphere

added theorem metric.closed_ball_eq_empty_iff_neg

added theorem metric.closed_ball_zero

added theorem metric.closure_ball_subset_closed_ball

added theorem metric.frontier_ball_subset_sphere

added theorem metric.frontier_closed_ball_subset_sphere

added def metric.sphere

added theorem metric.sphere_disjoint_ball

added theorem metric.sphere_subset_closed_ball

added theorem metric.sphere_union_ball

Modified src/topology/metric_space/closeds.lean