Commit 2021-10-18 09:32 39db98c8

View on Github →

feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top (#9727) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/analysis/convex/basic.lean

added theorem affine_subspace.convex

Modified src/analysis/convex/hull.lean

added theorem affine_span_convex_hull

modified theorem convex_hull_mono

added theorem convex_hull_subset_affine_span

Modified src/analysis/normed_space/add_torsor_bases.lean

added theorem interior_convex_hull_nonempty_iff_aff_span_eq_top

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_map.line_map_mem

added theorem affine_span_le

Modified src/topology/basic.lean

modified theorem interior_mono