sInf is minimum

Stream: Is there code for X?

[Ira Fesefeldt]

I am searching for a proof of something on the line

theorem sInf_of_finite {α : Type} [CompleteLinearOrder α] {s : Set α} (h_fin : Set.Finite s) (i : α) (P : α → Prop) :
    sInf {i ∈ s | P i } ∈ {i ∈ s | P i } := sorry

That is, the infimum on a finite set with a linear order is the minimum of the finite set.

Does something like this exist already?

[Ira Fesefeldt]

Nevermind, already found... Set.Nonempty.csInf_mem

[Kevin Buzzard]

Your theorem as it stands is false BTW:

import Mathlib

theorem sInf_of_finite {α : Type} [CompleteLinearOrder α] {s : Set α} (h_fin : Set.Finite s) (i : α) (P : α → Prop) :
    sInf {i ∈ s | P i } ∈ {i ∈ s | P i } := sorry

example : False := by
  have := sInf_of_finite (α := Fin 1) (s := ∅) (by simp) 0 (fun _ ↦ False)
  aesop

[Ira Fesefeldt]

Yes, nonempty is missing