Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-02 23:53 7e3e8834

View on Github →

chore(data/equiv): add docstrings (#7704)

add module docstrings
add def docstrings
rename decode2 to decode₂
squash some simps

Estimated changes

Modified scripts/nolints.txt

Modified src/computability/halting.lean

Modified src/computability/partrec.lean

deleted theorem partrec.bind_decode2_iff

added theorem partrec.bind_decode₂_iff

Modified src/computability/primrec.lean

Modified src/data/equiv/denumerable.lean

Modified src/data/equiv/encodable/basic.lean

modified def encodable.choose_x

deleted def encodable.decode2

deleted theorem encodable.decode2_inj

deleted theorem encodable.decode2_is_partial_inv

modified def encodable.decode_subtype

modified def encodable.decode_sum

added def encodable.decode₂

added theorem encodable.decode₂_inj

added theorem encodable.decode₂_is_partial_inv

added theorem encodable.decode₂_ne_none_iff

modified def encodable.encode'

modified def encodable.encode_subtype

modified def encodable.encode_sum

deleted theorem encodable.encodek2

added theorem encodable.encodek₂

deleted theorem encodable.mem_decode2'

deleted theorem encodable.mem_decode2

added theorem encodable.mem_decode₂'

added theorem encodable.mem_decode₂

Modified src/data/equiv/encodable/lattice.lean

deleted theorem encodable.Union_decode2

deleted theorem encodable.Union_decode2_cases

deleted theorem encodable.Union_decode2_disjoint_on

added theorem encodable.Union_decode₂

added theorem encodable.Union_decode₂_cases

added theorem encodable.Union_decode₂_disjoint_on

deleted theorem encodable.supr_decode2

added theorem encodable.supr_decode₂

Modified src/data/equiv/list.lean

modified def encodable.fintype_pi

Modified src/data/equiv/nat.lean

Modified src/measure_theory/measurable_space.lean

deleted theorem measurable_set.bUnion_decode2

added theorem measurable_set.bUnion_decode₂

Modified src/measure_theory/measure_space.lean

Modified src/measure_theory/outer_measure.lean

Modified src/measure_theory/pi_system.lean

Modified src/topology/algebra/infinite_sum.lean

deleted theorem tsum_Union_decode2

added theorem tsum_Union_decode₂

deleted theorem tsum_supr_decode2

added theorem tsum_supr_decode₂