Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.not_mem_range_self

Modification history

2017-11-22 05:33

data/finset/basic.lean

refactor(data/finset): redefine finsets as subtype of multisets

Modified finset.not_mem_range_self View on Github →

2017-10-15 01:58

data/finset/basic.lean

feat(*): working on list/basic, robusting simp proofs

Added finset.not_mem_range_self View on Github →