Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-11 18:53 257d1b7c

View on Github →

feat(*): preparations for Caratheodory's convexity theorem (#3030)

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.exists_pos_of_sum_zero_of_exists_nonzero

Modified src/algebra/ordered_field.lean

Modified src/data/equiv/basic.lean

added theorem equiv.set.apply_range_symm

added theorem equiv.set.sum_diff_subset_apply_inl

added theorem equiv.set.sum_diff_subset_apply_inr

added theorem equiv.set.sum_diff_subset_symm_apply_of_mem

added theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem

Modified src/data/finset.lean

added theorem finset.coe_mem

added theorem finset.filter_ne'

added theorem finset.filter_ne

added theorem finset.mk_coe

Modified src/data/set/basic.lean

added theorem set.coe_inclusion

Modified src/data/set/finite.lean

added theorem finset.finite_to_set_to_finset

Modified src/data/set/lattice.lean

added theorem set.subset_subset_Union

Modified src/linear_algebra/basis.lean

added theorem exists_sum_is_basis

added theorem linear_dependent_iff

Modified src/linear_algebra/dimension.lean

added theorem cardinal_le_dim_of_linear_independent'

added theorem cardinal_le_dim_of_linear_independent

Modified src/logic/embedding.lean

added def function.embedding.inl

added def function.embedding.inr