Commit 2024-02-25 13:35 23adc289

View on Github →

chore: fix port of join_filter_isEmpty_eq_false (#10951)

Estimated changes

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Data/List/Join.lean

deleted theorem List.join_filter_isEmpty_eq_false

added theorem List.join_filter_not_isEmpty