Commit 2022-11-09 14:43 d9a51803

refactor(linear_algebra,analysis/normed_space): use finite, review API, golf (#17320)

• replace fintype_of_fin_dim_affine_independent with finite_of_fin_dim_affine_independent;
• rename old finite_of_fin_dim_affine_independent to finite_set_of_fin_dim_affine_independent, generalize;
• define affine_basis.comp_equiv;
• add affine_basis.finite, affine_basis.finite_set, affine_basis.coord_apply_centroid, affine_basis.card_eq_finrank_add_one
• use more precise statement in exists_affine_basis, add exists_affine_subbasis;
• rename interior_convex_hull_aff_basis to affine_basis.interior_convex_hull;
• rename exists_subset_affine_independent_span_eq_top_of_open to is_open.exists_between_affine_independent_span_eq_top, golf;
• add is_open.exists_subset_affine_independent_span_eq_top, is_open.affine_span_eq_top, affine_span_eq_top_of_nonempty_interior, and affine_basis.centroid_mem_interior_convex_hull;
• rename interior_convex_hull_nonempty_iff_aff_span_eq_top to interior_convex_hull_nonempty_iff_affine_span_eq_top