Theorems · Theorem · order theory
Finset.sup_empty
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, ∅.sup f = ⊥- Defined in
- Mathlib.Data.Finset.Lattice.Fold
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
- Assumes
- SemilatticeSupOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Bot.botstatement · cited by 4,720
- OrderBotstatement and proof · cited by 1,055
- SemilatticeSupstatement and proof · cited by 785
- Finset.supstatement · cited by 530
- Finset.fold_emptyproof · cited by 3
Cited by72
Results whose statement or proof uses this declaration.
- MonomialOrder.degree_zeroproof · cited by 29
- MonomialOrder.leadingCoeff_zeroproof · cited by 14
- MonomialOrder.degree_monomialproof · cited by 12
- Polynomial.degree_sum_leproof · cited by 11
- Seminorm.finset_sup_applyproof · cited by 7
- AddMonoidAlgebra.supDegree_zeroproof · cited by 5
- partialSups_disjointedproof · cited by 5
- CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSupproof · cited by 4
- Finset.mem_supproof · cited by 4
- WithSeminorms.isVonNBounded_iff_seminorm_boundedproof · cited by 4
- Module.End.independent_genEigenspaceproof · cited by 4
- Finset.sup_eq_bot_iffproof · cited by 4