ENat.iInf_eq_nat_iff

Stream: Is there code for X?

[Iván Renison]

Hi, do you know if there is a lemma saying something like this?

lemma ENat.iInf_eq_nat_iff {ι : Sort*} {f : ι → ℕ} {n : ℕ} :
    ⨅ i, (f i : ℕ∞) = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := sorry

[Jakub Nowak]

Seems like we don't even have a generic version of this. iInf_eq_of_forall_ge_of_forall_gt_exists_lt seems to be the closest.
We might want to have

{α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ι → α} {b : α} : (∀ (i : ι), b ≤ f i) → (∃ i, f i = b) → ⨅ i, f i = b

[Kevin Buzzard]

(deleted)

[Ruben Van de Velde]

Not sure this helps, but too tired to solve the last sorry

import Mathlib
lemma ENat.iInf_eq_nat_iff {ι : Sort*} {f : ι → ℕ} {n : ℕ} :
    ⨅ i, (f i : ℕ∞) = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := by
  by_cases! hι : IsEmpty ι
  · simp
  rw [← ENat.coe_iInf]
  simp
  constructor
  · rintro rfl
    constructor
    · sorry
    · intro i
      apply ciInf_le
      simp
  · rintro ⟨⟨j, rfl⟩, h⟩
    apply le_antisymm
    · apply ciInf_le
      simp
    · apply le_ciInf h

[Iván Renison]

It helps, although that sorry seems difficult. I will try to probe it

[Jakub Nowak]

You can replace

  rw [← ENat.coe_iInf]
  simp

with

  norm_cast

[Snir Broshi]

The last sorry is exact ciInf_mem f

[Jakub Nowak]

Heh, you were just few seconds faster. I'm wondering why exact? couldn't find it?

[Jakub Nowak]

I'm guessing it can't see past Membership to know that it's just function application?

[Snir Broshi]

golf

import Mathlib
lemma ENat.iInf_eq_nat_iff {ι : Sort*} {f : ι → ℕ} {n : ℕ} :
    ⨅ i, (f i : ℕ∞) = n ↔ (∃ i, f i = n) ∧ ∀ i, n ≤ f i := by
  cases isEmpty_or_nonempty ι
  · simp
  norm_cast
  refine ⟨(· ▸ ⟨ciInf_mem f, fun _ ↦ ciInf_le (OrderBot.bddBelow ..) _⟩), fun ⟨⟨i, hi⟩, h⟩ ↦ ?_⟩
  exact le_antisymm (hi ▸ ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

[Jakub Nowak]

Should we add ∃ i, f i = ⨅ i, f i to mathlib?

[Snir Broshi]

For which type/class? This isn't always true

[Jakub Nowak]

[ConditionallyCompleteLinearOrder α] [WellFoundedLT α]

[Snir Broshi]

(e.g. the infimum of all the negative integers is zero)

[Snir Broshi]

Jakub Nowak said:

[ConditionallyCompleteLinearOrder α] [WellFoundedLT α]

Do you mean as a simple rephrasing of docs#ciInf_mem ?

[Jakub Nowak]

Yes. Only for it to be found by exact?.

[Snir Broshi]

idk, just swapping the equality in that statement is enough to fool exact?, we should improve its algorithm rather than adding small translation lemmas

[Aaron Liu]

I believe the correct hypothesis for that one is not being a docs#Order.IsPredPrelimit

[Violeta Hernández]

Seems like you're describing docs#csInf_mem_of_not_isPredPrelimit

[Iván Renison]

And should we add ENat.iInf_eq_nat_iff to Mathlib?

[Iván Renison]

I opened #34144 adding ENat.iInf_eq_nat_iff

[Jakub Nowak]

Doesn't it trivially generalizes to any α instead of ℕ, and WithTop α instead of ℕ∞?

[Iván Renison]

Maybe with some assumptions on α, or you think that with out?

[Jakub Nowak]

Yeah, sorry, I just assumed implicitly "throw in all instances the proof requires". That would be [ConditionallyCompleteLinearOrder α] [WellFoundedLT α] I think?

[Jakub Nowak]

@Aaron Liu suggest we could do better assumptions, but that would be extra effort.

[Iván Renison]

Ok, yes