directedness of <

Stream: Is there code for X?

[Mario Carneiro]

import Mathlib.Data.Real.Basic

example (f : α → ℝ) (l : List α) : ∃ a, ∀ x ∈ l, a < f x := sorry

is there a short proof of this using directed sets or filters?

[Yakov Pechersky]

Brute force =C

import Mathlib.Data.Real.Basic

example (f : α → ℝ) (l : List α) : ∃ a, ∀ x ∈ l, a < f x := by
  cases hl : List.minimum? (List.map f l) with
  | none => simp_all
  | some a =>
      have : Antisymm fun (x y : ℝ) => x ≤ y := ⟨le_antisymm⟩
      rw [List.minimum?_eq_some_iff] at hl
      · refine ⟨a - 1, fun x hx => ?_⟩
        refine (sub_lt_self a one_pos).trans_le (hl.right _ _)
        exact List.mem_map_of_mem _ _
      · simp
      · exact min_choice
      · simp

[Kevin Buzzard]

Use boundedness?

import Mathlib

variable {α : Type*}

theorem foo (S : Set ℝ) (hS : Bornology.IsBounded S) : ∃ a : ℝ, ∀ s ∈ S, a < s := by sorry


example (f : α → ℝ) (l : List α) : ∃ a, ∀ x ∈ l, a < f x := by
  obtain ⟨a, ha⟩ := foo {x | x ∈ (List.map f l)} <| Set.Finite.isBounded <| List.finite_toSet (List.map f l)
  aesop

[Kevin Buzzard]

-- surely this should be in the library?
theorem foo (S : Set ℝ) (hS : Bornology.IsBounded S) : ∃ a : ℝ, ∀ s ∈ S, a < s :=
match isEmpty_or_nonempty S with
| Or.inl ⟨h⟩ => ⟨37, fun x hx ↦ (h ⟨x, hx⟩).elim⟩
| Or.inr ⟨x, hx⟩ => by
  cases hS with
  | intro w h =>
    use x - w - 37
    intros s hs
    simp only [compl_compl] at h
    specialize h hs hx
    rw [abs_le] at h
    linarith

[Junyan Xu]

import Mathlib.Data.Real.Basic
import Mathlib.Data.List.MinMax

example (f : α → ℝ) (l : List α) : ∃ a, ∀ x ∈ l, a < f x := by
  cases' l with a l; · simp
  use ((a :: l).map f).minimum_of_length_pos (by simp) - 1
  exact fun x hx ↦ (sub_one_lt _).trans_le (List.minimum_of_length_pos_le_of_mem
    (List.mem_map_of_mem _ hx) _)

(docs#List.minimum_of_length_pos does not follow naming convention)

[Yury G. Kudryashov]

See docs#Set.exists_lower_bound_image

[Yury G. Kudryashov]

Sorry, wrong Nonempty assumption

[Yury G. Kudryashov]

docs#Finset.exists_le

[Antoine Chambert-Loir]

Yes, and since Mario needs <, one just needs to add that ℝ doesn't have a least element.

[Mario Carneiro]

here's what I would consider the "baseline" proof, by induction:

theorem exists_lt_list (l : List α) (f : α → ℝ) : ∃ a, ∀ x ∈ l, a < f x := by
  induction' l with a l ih <;> simp
  have ⟨r, h⟩ := ih
  refine ⟨min (f a - 1) r, by simp (config := {contextual := true}) [h]⟩

(unfortunately many of the suggestions seem to involve a lot more work than this just to do the finessing at the end)

[Mario Carneiro]

here's a proof using Finset.exists_le, which is going the wrong direction (it shows upper bounds, not lower bounds):

example (l : List α) (f : α → ℝ) : ∃ a, ∀ x ∈ l, a < f x := by
  have ⟨a, ha⟩ := Finset.exists_le (l.map (-f ·)).toFinset
  exact ⟨-a-1, fun _ h => by simp at ha; linarith [ha _ h]⟩

[Antoine Chambert-Loir]

It seems reasonable to add a Finset.exists_ge lemma.

[Yury G. Kudryashov]

As well as exists_lt and exists_gt.