Theorems · Theorem · order theory
Set.exists_min_image
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] (s : Set α) (f : α → β),
s.Finite → s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b- Defined in
- Mathlib.Data.Set.Finite.Lemmas
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 82 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- LinearOrderstatement and proof · cited by 8,572
- Set.Nonemptystatement and proof · cited by 2,627
- Set.Finitestatement and proof · cited by 1,814
- Set.Finite.toFinsetproof · cited by 351
- Set.Finite.mem_toFinsetproof · cited by 74
- Finset.exists_min_imageproof · cited by 7
Cited by4
Results whose statement or proof uses this declaration.
- Filter.Tendsto.exists_within_forall_leproof · cited by 3
- Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrationalproof · cited by 2
- Northcott.exists_min_imageproof · cited by 2
- Set.exists_lower_bound_imageproof · cited by 2