Commit 2022-12-14 02:02 e2fdb6aa

View on Github →

feat: port control.traversable.lemmas (#948) Port of control.traversable.lemmas Based on 3342d1b2178381196f818146ff79bc0e7ccd9e2d

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Traversable/Lemmas.lean

added def Traversable.PureTransformation

added theorem Traversable.comp_sequence

added theorem Traversable.id_sequence

added theorem Traversable.map_eq_traverse_id

added theorem Traversable.map_traverse'

added theorem Traversable.map_traverse

added theorem Traversable.naturality'

added theorem Traversable.naturality_pf

added theorem Traversable.pure_transformation_apply

added theorem Traversable.pure_traverse

added theorem Traversable.traverse_comp

added theorem Traversable.traverse_eq_map_id'

added theorem Traversable.traverse_id

added theorem Traversable.traverse_map'

added theorem Traversable.traverse_map