Theorems · Theorem · order theory
Finset.map_toDual_max
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α),
WithBot.map (⇑OrderDual.toDual) s.max = (Finset.image (⇑OrderDual.toDual) s).min- Defined in
- Mathlib.Data.Finset.Max
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- LinearOrderstatement and proof · cited by 8,572
- Equivstatement · cited by 8,337
- WithTopproof · cited by 3,754
- WithBotstatement · cited by 1,498
- WithTop.someproof · cited by 1,128
- OrderDualstatement and proof · cited by 927
- Finset.imagestatement and proof · cited by 910
- OrderDual.toDualstatement and proof · cited by 481
- WithBot.mapstatement and proof · cited by 66
- Finset.maxstatement and proof · cited by 50
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.