Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 08:46 d0820017

View on Github →

feat(analysis/convex/independent): convex independence (#9018)

Estimated changes

Created src/analysis/convex/independent.lean

added theorem convex.extreme_points_convex_independent

added theorem convex_independent.comp_embedding

added def convex_independent

added theorem convex_independent_iff_finset

added theorem convex_independent_iff_not_mem_convex_hull_diff

added theorem convex_independent_set_iff_inter_convex_hull_subset

added theorem convex_independent_set_iff_not_mem_convex_hull_diff

added theorem function.injective.convex_independent_iff_set

added theorem subsingleton.convex_independent

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine_independent.indicator_eq_of_affine_combination_eq