max = iSup

Stream: mathlib4

[Michael Stoll]

How do I prove this in Mathlib?

import Mathlib.Data.Fin.VecNotation
import Mathlib.Order.CompletePartialOrder
import Mathlib.Order.ConditionallyCompleteLattice.Basic

example {α} [CompleteLinearOrder α] (a b : α) : max a b = iSup fun i ↦ ![a, b] i := by
  sorry

(In my use case, a and b are NNReals.)

[Ruben Van de Velde]

docs#sup_eq_iSup ?

[Michael Stoll]

But this has Bool as index type, not Fin 2.

[Yaël Dillies]

A very general trick for these kinds of situation is to use the universal property

[Michael Stoll]

Which universal property of what?

[Yaël Dillies]

(also may I complain of MWEs importing Mathlib? I've now been waiting for three minutes getting the entire cache)

[Michael Stoll]

Sorry, I was too lazy to minimize the imports. (It doesn't take long on the live web page, though.)

[Yaël Dillies]

import Mathlib.Data.Fin.VecNotation
import Mathlib.Order.ConditionallyCompleteLattice.Basic

example {α} [CompleteLinearOrder α] (a b : α) : max a b = iSup fun i ↦ ![a, b] i :=
  eq_of_forall_ge_iff <| by simp [Fin.forall_fin_two]

[Ruben Van de Velde]

import Mathlib

example {α} [CompleteLinearOrder α] (a b : α) : max a b = iSup fun i ↦ ![a, b] i := by
  --rw [<- sup_iSup_nat_succ]
  rw [sup_comm]
  rw [sup_eq_iSup]
  apply Equiv.iSup_congr finTwoEquiv.symm
  intro x
  cases x<;>
  simp [finTwoEquiv]

[Ruben Van de Velde]

But Yaël's approach clearly works too

[Michael Stoll]

Would it make sense to have that in Mathlib (together with the Inf version)?

[Ruben Van de Velde]

(seems like there are no lemmas about finTwoEquiv)

[Yaël Dillies]

I think the better lemma to have is Set.range ![a, b] = {a, b}, as then you can unfold docs#iSup and rewrite using docs#sSup_pair

[Yaël Dillies]

I just think there are too many variants of such lemmas for them to be worth having

[Yaël Dillies]

What we should have instead is some reflection-like handling of vector notation, so that eg iSup ![a, b, c, d, e] = a ⊔ b ⊔ c ⊔ d ⊔ e can be proved easily. Maybe a simproc? Maybe carefully chosen simp lemmas?

[Ruben Van de Velde]

Something close to docs#Fin.range_cons ?

[Michael Stoll]

Why is NNReal not a CompleteLinearOrder?
I just noticed that I can't apply the lemma to my use case :frown:

[Bhavik Mehta]

It doesn't have suprema of unbounded above sets - it is a conditionally complete linear order instead

[Kevin Buzzard]

Because the naturals has no sup? I guess ENNReal will be the complete one.

[Michael Stoll]

OK, so what are the necessary type class assumptions then? (Yaël's proof seems to break down for NNReals.)

[Michael Stoll]

Ruben's proof also breaks down. So how to prove what I actually want:

import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.NNReal.Defs

open NNReal

lemma foo (a b : ℝ≥0) : max a b = iSup fun i ↦ ![a, b] i := by
  sorry

[Bhavik Mehta]

import Mathlib.Data.Fin.VecNotation
import Mathlib.Order.ConditionallyCompleteLattice.Indexed

example {α} [ConditionallyCompleteLinearOrder α] (a b : α) : max a b = iSup fun i ↦ ![a, b] i :=
  eq_of_forall_ge_iff <| by simp [ciSup_le_iff, Fin.forall_fin_two]

[Michael Stoll]

Somehow I think this should be easier (say, simp should be able to do that...).

[Michael Stoll]

I guess that comes back to Yaël's suggestion further above..

[Bhavik Mehta]

ConditionallyCompleteLattice actually works in place of ConditionallyCompleteLinearOrder

[Yaël Dillies]

Bhavik Mehta said:

[...]

As stated above, using the universal property is a very versatile proof strategy :wink:

[Yaël Dillies]

Michael Stoll said:

asier (say, simp should be able to do that...).

I actually don't know why docs#ciSup_le_iff isn't simp