Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 09:20 d55a6545

View on Github →

feat(order/*): Order constructions under to_dual/of_dual (#13788) A few missing lemmas about of_dual and to_dual.

Estimated changes

added theorem finset.map_of_dual_max
added theorem finset.map_of_dual_min
added theorem finset.map_to_dual_max
added theorem finset.map_to_dual_min
added theorem finset.of_dual_inf'
added theorem finset.of_dual_inf
added theorem finset.of_dual_max'
added theorem finset.of_dual_min'
added theorem finset.of_dual_sup'
added theorem finset.of_dual_sup
added theorem finset.to_dual_inf'
added theorem finset.to_dual_inf
added theorem finset.to_dual_max'
added theorem finset.to_dual_min'
added theorem finset.to_dual_sup'
added theorem finset.to_dual_sup
added theorem of_dual_compl
added theorem to_dual_compl
added theorem of_dual_bot
added theorem of_dual_top
added theorem to_dual_bot
added theorem to_dual_top
added theorem of_dual_inf
added theorem of_dual_max
added theorem of_dual_min
added theorem of_dual_sup
added theorem to_dual_inf
added theorem to_dual_max
added theorem to_dual_min
added theorem to_dual_sup