Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 da7bbd7f

View on Github →

feat(data/set): add set.pi

Estimated changes

Modified data/equiv/basic.lean

added def equiv.pi_equiv_subtype_sigma

Modified data/equiv/list.lean

added def encodable.fintype_arrow

added def encodable.fintype_pi

Modified data/finset.lean

added theorem finset.set_of_mem

Modified data/fintype.lean

added theorem finset.coe_univ

Modified data/set/basic.lean

added def set.pi

added theorem set.pi_empty_index

added theorem set.pi_if

added theorem set.pi_insert_index

added theorem set.pi_singleton_index

added theorem set.sep_set_of

added theorem set.sep_univ

added theorem set.set_of_mem

Modified data/set/countable.lean

added theorem set.countable_pi

Modified data/set/lattice.lean

added theorem set.pi_def

Modified logic/basic.lean

added theorem rec_heq_of_heq