iInf pos for finite sets

Stream: mathlib4

[Emilie (Shad Amethyst)]

I cannot seem to find a way to prove the following:

example {ι : Type*} [Finite ι] [Nonempty ι] {f : ι → ℝ} (forall_pos : ∀ i : ι, 0 < f i) : 0 < iInf f := by
  sorry

This should intuitively be true, and I'm confused as to why I struggle to prove it too, since it should just be a matter of proving it by induction on ι

[Eric Wieser]

What if ι is empty?

[Emilie (Shad Amethyst)]

Right, I forgot this assumption; in my case ι is Nonempty

[Ruben Van de Velde]

Does it work to contrapose and apply docs#iInf_le with your arbitrary element from iota?

[Yaël Dillies]

No, because that wouldn't use finiteness

[Yaël Dillies]

1, 1/2, 1/3, ... is a sequence of strictly positive reals whose infimum is zero

[Emilie (Shad Amethyst)]

After taking a small break, I have the following proof for this fact:

variable {α : Type*} [ConditionallyCompleteLinearOrder α] in
lemma lt_csInf_finset {s : Finset α} {a : α} (s_ne : s.Nonempty) (hs : ∀ x ∈ s, a < x) :
    a < sInf (s : Set α) := by
  induction s_ne using Finset.Nonempty.cons_induction
  case h₀ x => simpa using hs
  case h₁ x s x_notin_s s_ne ih =>
    simp only [Finset.cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
    rw [Finset.cons_eq_insert, Finset.coe_insert, csInf_insert (Finset.bddBelow s) s_ne]
    exact lt_inf_iff.mpr ⟨hs.left, ih hs.right⟩

variable {α : Type*} [ConditionallyCompleteLinearOrder α] in
theorem lt_csInf_of_finite {s : Set α} {a : α} (s_fin : s.Finite) (s_ne : s.Nonempty)
    (hs : ∀ x ∈ s, a < x) : a < sInf s := by
  let ⟨finset, s_eq⟩ := s_fin.exists_finset_coe
  rw [← s_eq]
  apply lt_csInf_finset
  · rwa [← s_eq] at s_ne
  · simpa [← s_eq, Finset.mem_coe] using hs

variable {α : Type*} [ConditionallyCompleteLinearOrder α] in
theorem lt_ciInf_of_finite {ι : Type*} [Fintype ι] [Nonempty ι] {f : ι → α} {a : α}
    (hf : ∀ i : ι, a < f i) : a < iInf f := by
  rw [← sInf_range]
  apply lt_csInf_of_finite (finite_range f) (range_nonempty f)
  simpa

[Richard Copley]

(I was having fun looking at this and didn't notice your message.) A useful lemma already in Mathlib is Finset.Nonempty.cInf_eq_min':

import Mathlib.Data.Finset.Lattice
import Mathlib.Order.ConditionallyCompleteLattice.Finset
import Mathlib.Data.Real.Archimedean

example {ι : Type*} [Finite ι] [Nonempty ι] {f : ι → ℝ} (forall_pos : ∀ i : ι, 0 < f i) : 0 < iInf f := by
  have H (s : Finset ℝ) (he : Finset.Nonempty s) (h : ∀ x ∈ s, 0 < x) : 0 < sInf (s : Set ℝ) := by
    rewrite [Finset.Nonempty.cInf_eq_min' he]
    rewrite [Finset.lt_min'_iff]
    exact h
  have ⟨s, hs⟩ := Set.Finite.exists_finset_coe <| Set.finite_range f
  have hne : Finset.Nonempty s := by
    rewrite [← Finset.coe_nonempty, hs]
    exact Set.range_nonempty f
  have : ∀ x ∈ s, 0 < x := by
    intro x hx
    rewrite [← Finset.mem_coe, hs] at hx
    have ⟨i, hi⟩ := hx
    exact hi ▸ forall_pos i
  rewrite [iInf, ← hs]
  exact H s hne this

[Emilie (Shad Amethyst)]

Ah, well there's lt_cInf_iff

[Emilie (Shad Amethyst)]

Darn, I was only searching for csInf and ciInf, so at no point it yielded results about cInf

[Emilie (Shad Amethyst)]

Gotta fix those names

[Eric Wieser]

cInf is a porting error