Zulip Chat Archive

Stream: Is there code for X?

Topic: element of nonempty set with smallest height

Kevin Buzzard (Mar 13 2023 at 13:25):

I just found myself writing this for my class today:

import tactic

open_locale classical

/-- If a type A is equipped with an ℕ-valued "height function" `h` and a subset `S`,
and if `hs` is a proof that `S` is nonempty, then `smallest_height h hs`
returns an element of `S` with smallest height. The proof that it has smallest
height is `smallest_height_spec h hs`. -/
noncomputable def smallest_height {A : Type} (h : A → ℕ) {S : set A}
  (hs : set.nonempty S) : S :=
have hn' : ∃ s, s ∈ S ∧ h s = nat.find _ := nat.find_spec (hs.image h),
⟨Exists.some hn', (Exists.some_spec hn').1⟩

lemma smallest_height_spec {A : Type} (h : A → ℕ) {S : set A}
  (hs : set.nonempty S) (s : A) (hsS : s ∈ S): h (smallest_height h hs).1 ≤ h s :=
begin
  have hn' : ∃ s, s ∈ S ∧ h s = nat.find _ := nat.find_spec (hs.image h),
  have h2 := (Exists.some_spec hn').2,
  convert nat.find_min' (hs.image h) (show h s ∈ h '' S, from ⟨s, hsS, rfl⟩),
end