Theorems · Theorem · order theory
Finset.map_toDual_min
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α),
WithTop.map (⇑OrderDual.toDual) s.min = (Finset.image (⇑OrderDual.toDual) s).max- Defined in
- Mathlib.Data.Finset.Max
- Cited by
- 1 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
- WithTopstatement · cited by 3,754
- WithBotproof · cited by 1,498
- OrderDualstatement and proof · cited by 927
- Finset.imagestatement and proof · cited by 910
- WithBot.someproof · cited by 541
- OrderDual.toDualstatement and proof · cited by 481
- WithTop.mapstatement and proof · cited by 68
- Finset.maxstatement · cited by 50
Cited by1
Results whose statement or proof uses this declaration.
- Finset.min_erase_ne_selfproof · cited by 0