Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-09 22:58 baa3aa73

View on Github →

refactor(data/set/basic): change def of ⊂ to match < (#1862)

Estimated changes

Modified src/data/finset.lean

Modified src/data/set/basic.lean

added theorem set.eq_or_ssubset_of_subset

added theorem set.nonempty_diff

modified theorem set.not_subset

modified theorem set.ssubset_def

added theorem set.ssubset_iff_subset_ne

deleted theorem set.ssubset_iff_subset_not_subset

modified def set.strict_subset

Modified src/data/set/finite.lean

Modified src/data/set/lattice.lean

Modified src/linear_algebra/basic.lean

added theorem submodule.exists_of_lt

modified theorem submodule.le_def'

modified theorem submodule.le_def

added theorem submodule.lt_def

added theorem submodule.lt_iff_le_and_exists

added theorem submodule.not_le_iff_exists

modified def submodule.of_le

modified theorem submodule.of_le_apply

Modified src/order/zorn.lean