Minimum of Finset

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I have an assumption of the form h: ∀ i ∈ I, ∃ t, 0 < t ∧ Metric.ball (f i) t ⊆ u i and I want to get ∃ ε, 0 < ε ∧ ∀ i ∈ I, Metric.ball (f i) ε ⊆ u i.

I is a Finset so I think it should be possible by taking a "finite list " of elements that satisfies h, one for every i ∈ I, and then taking its minimum, but I don't know how to formalice this.

Is there any simple way of doing it?

Thanks in advance

[Eric Wieser]

does choose t ht using h work?

[Esteban Martínez Vañó]

It produces a function t of type t : (i : H) → i ∈ I → ℝ (where I : Finset H) and the corresponding proposition, but I don't know how to conclude from it.

I've managed to prove it in this way, but I'm sure it can be improved so feel free to do it please :)

theorem aux {ι X : Type} [MetricSpace X] (I: Finset ι) (f: ι → X) (u: ι → Set X) (h: ∀ i ∈ I, ∃ (t : ℝ), (0 < t ∧ Metric.ball (f i) t ⊆ u i)):
  ∃ (ε : ℝ), (0 < ε ∧ ∀ i ∈ I, Metric.ball (f i) ε ⊆ u i) := by
    rcases Classical.em (I.Nonempty) with Inem | Iem
    · let F : ι → ℝ := fun i ↦ if p: ∃ t, 0 < t ∧ Metric.ball (f i) t ⊆ u i then Classical.choose p else 0
      let T := Finset.image F I
      have Tnem: T.Nonempty := by
        apply Finset.Nonempty.image
        assumption
      let ε := Finset.min' T Tnem
      have εinT: ε ∈ T := by
        apply Finset.min'_mem
      dsimp [T] at εinT
      rw [Finset.mem_image] at εinT
      rcases εinT with ⟨i₀, i₀inI, εeqFi₀⟩
      use ε
      constructor
      · dsimp [F] at εeqFi₀
        rw [dif_pos (h i₀ i₀inI)] at εeqFi₀
        have := Classical.choose_spec (h i₀ i₀inI)
        rw [← εeqFi₀]
        exact this.1
      · intro i iinI
        let t := F i
        have : 0 < t ∧ Metric.ball (f i) t ⊆ u i := by
          dsimp [t, F]
          rw [dif_pos (h i iinI)]
          exact Classical.choose_spec (h i iinI)
        apply le_trans _ this.2
        apply Metric.ball_subset_ball
        have tinT : t ∈ T := by
          rw [Finset.mem_image]
          use i, iinI
        exact Finset.min'_le T t tinT
    · rw [Finset.not_nonempty_iff_eq_empty] at Iem
      use 1
      constructor
      · linarith
      · intro i iinI
        rw [Iem] at iinI
        contradiction

[David Loeffler]

Nothing like a quick round of golf to relax on a summer afternoon :-)

open Finset in
theorem aux {ι X : Type} [MetricSpace X] (I : Finset ι) (f : ι → X) (u : ι → Set X)
    (h: ∀ i ∈ I, ∃ (t : ℝ), (0 < t ∧ Metric.ball (f i) t ⊆ u i)):
    ∃ (ε : ℝ), (0 < ε ∧ ∀ i ∈ I, Metric.ball (f i) ε ⊆ u i) := by
  choose t ht using h
  by_cases hI : Finset.Nonempty I; swap
  · rw [nonempty_iff_ne_empty, Ne, not_not] at hI
    exact ⟨1, zero_lt_one, fun i hi ↦ (not_mem_empty _ (hI ▸ hi)).elim⟩
  obtain ⟨⟨j, hj⟩, -, hj'⟩ := exists_min_image univ (fun i : I ↦ t i.1 i.2) (by simpa using hI)
  refine ⟨t j hj,  (ht j hj).1, fun i hi ↦ ?_⟩
  exact (Metric.ball_subset_ball <| hj' ⟨i, hi⟩ (mem_univ _)).trans (ht i hi).2

Other than superficial golfing (using refine ⟨...⟩ to shorten constructor applications, etc), the main difference to what you wrote is the lemma Finset.exists_min_imagewhich automates several steps from your proof.