Commit 2025-01-31 21:28 41fd5d11

View on Github →

feat: generalize mem_dite to Membership α β (#21262)

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Set.mem_dite

Modified Mathlib/Logic/Basic.lean

added theorem dite_mem

added theorem ite_mem

added theorem mem_dite

added theorem mem_ite