English
If s is nonempty, then the supremum s.sup f lies in the image of f on s.
Русский
Если s непусто, то $s.sup f$ принадлежит образу функции f на множестве s.
LaTeX
$$$s.Nonempty \rightarrow s.sup f \in f''s$$$
Lean4
theorem sup_mem_of_nonempty (hs : s.Nonempty) : s.sup f ∈ f '' s := by
classical
induction s using Finset.induction with
| empty => simp only [Finset.not_nonempty_empty] at hs
| insert a s _ h =>
rw [Finset.sup_insert (b := a) (s := s) (f := f)]
cases s.eq_empty_or_nonempty with
| inl hs => simp [hs]
| inr hs =>
simp only [Finset.coe_insert]
rcases le_total (f a) (s.sup f) with (ha | ha)
· rw [sup_eq_right.mpr ha]
exact Set.image_mono (Set.subset_insert a s) (h hs)
· rw [sup_eq_left.mpr ha]
apply Set.mem_image_of_mem _ (Set.mem_insert a ↑s)
