Mathlib Changelog
v3
Changelog
About
Github
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