Theorems · Theorem · order theory
Finset.exists_mem_eq_sup
∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] (s : Finset ι),
s.Nonempty → ∀ (f : ι → α), ∃ i ∈ s, s.sup f = f i- Defined in
- Mathlib.Data.Finset.Lattice.Fold
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- LinearOrderstatement and proof · cited by 8,572
- OrderBotstatement and proof · cited by 1,055
- Finset.Nonemptystatement and proof · cited by 1,001
- Finset.supstatement · cited by 530
- Finset.sup'_eq_supproof · cited by 35
- Finset.exists_mem_eq_sup'proof · cited by 9
Cited by11
Results whose statement or proof uses this declaration.
- AddMonoidAlgebra.exists_supDegree_mem_supportproof · cited by 4
- Seminorm.exists_apply_eq_finset_supproof · cited by 2
- Polynomial.degree_sum_eq_of_disjointproof · cited by 2
- AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree'proof · cited by 1
- IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_neproof · cited by 1
- IsUltrametricDist.nnnorm_sum_eq_sup_of_pairwise_neproof · cited by 1
- MvPolynomial.totalDegree_add_eq_left_of_totalDegree_ltproof · cited by 1
- MvPolynomial.degreeOf_add_eq_of_degreeOf_ltproof · cited by 1
- IsGreatest.pi_normproof · cited by 1
- IsGreatest.pi_norm'proof · cited by 1
- MvPolynomial.totalDegree_coeff_finSuccEquiv_add_leproof · cited by 0