Commit 2024-01-29 07:53 86ffe042

View on Github →

chore(Order/Filter/ListTraverse): move from Basic (#10048)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.mem_traverse

deleted theorem Filter.mem_traverse_iff

deleted theorem Filter.sequence_mono

Created Mathlib/Order/Filter/ListTraverse.lean

added theorem Filter.mem_traverse

added theorem Filter.mem_traverse_iff

added theorem Filter.sequence_mono

Modified Mathlib/Topology/List.lean