exists list in set with length le all in set

Stream: Is there code for X?

[Paige Thomas]

I think this should hold, maybe by well ordering, but I'm struggling to prove it:

lemma min_list_length_exists
  {α : Type}
  (S : Set (List α))
  (h1 : S.Nonempty) :
  ∃ (xs : List α), xs ∈ S ∧ ∀ (ys : Str α), ys ∈ S → xs.length <= ys.length :=
  by

[Yakov Pechersky]

Informally, consider the image of S under List.length. There is a list in S that takes the value of the infimum of that length '' S, since S is nonempty and thus the image is nonempty, and length '' S is in Nat, where set infima are in the set afaiu. The existence of the list is the first part, and the fact that the length of it is a lower bound is the fact that the length is the infimum.

[Daniel Weber]

Here's a formalization of that:

import Mathlib

lemma min_list_length_exists {α : Type} (S : Set (List α)) (h1 : S.Nonempty) :
    ∃ (xs : List α), xs ∈ S ∧ ∀ (ys : List α), ys ∈ S → xs.length <= ys.length :=
  have ⟨x, hx, hv⟩ := Nat.sInf_mem <| h1.image _
  ⟨x, hx, fun _ hy ↦ hv ▸ Nat.sInf_le <| Set.mem_image_of_mem List.length hy⟩

[Paige Thomas]

Awesome! Thank you both!