Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 06:24 b0fe3cd2

View on Github →

feat(order/filter): add filter.coprod_bot etc (#13662)

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.bot_coprod

added theorem filter.bot_coprod_bot

added theorem filter.coprod_bot

Modified src/order/filter/pi.lean

added theorem filter.Coprod_bot'

added theorem filter.Coprod_bot

added theorem filter.Coprod_eq_bot_iff'

added theorem filter.Coprod_eq_bot_iff