Monotone function maps iSup to iSup

Stream: Is there code for X?

[Michael Stoll]

Do we have something like the following?

example {α β ι : Type*} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β]
    [Finite ι] [Nonempty ι] (f : ι → α) (g : α → β) (hg : Monotone g) :
    g (⨆ i, f i) = ⨆ i, g (f i) := by
  sorry

[Snir Broshi]

Is this it?
https://github.com/leanprover-community/mathlib4/pull/35669/files#diff-a2d7cd0fc622232f710791d17556cd9c2453f0794c595d23b5ef2383bb10db23R59-R60

[Snir Broshi]

(#Is there code for X? > `sSup (f '' s) = f (sSup s) `)

[Snir Broshi]

If so then β doesn't have to have a linear order, it can be ConditionallyCompleteLattice

[Michael Stoll]

It's close, modulo converting to an docs#sSup . Maybe you can add ciSup versions (perhaps in the Finite namespace, similar to what I'm doing in #35260), too?

[Michael Stoll]

Relative to my PR, this would add

namespace Finite

variable {α β ι : Type*} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β]
  [Finite ι] [Nonempty ι]

lemma map_iSup_of_monotone (f : ι → α) {g : α → β} (hg : Monotone g) :
    g (⨆ i, f i) = ⨆ i, g (f i) := by
  refine le_antisymm ?_ ?_
  · obtain ⟨j, hj⟩ : ∃ j, f j = ⨆ i, f i := exists_eq_ciSup_of_finite
    rw [← hj]
    exact Finite.le_ciSup_of_le j le_rfl
  · exact ciSup_le fun i ↦ hg <| Finite.le_ciSup f i

lemma map_iInf_of_monotone (f : ι → α) {g : α → β} (hg : Monotone g) :
    g (⨅ i, f i) = ⨅ i, g (f i) :=
  map_iSup_of_monotone (α := αᵒᵈ) (β := βᵒᵈ) f fun _ _ h ↦ hg h

lemma map_iSup_of_antitone (f : ι → α) {g : α → β} (hg : Antitone g) :
    g (⨆ i, f i) = ⨅ i, g (f i) :=
  map_iSup_of_monotone (β := βᵒᵈ) f hg

lemma map_iInf_of_antitone (f : ι → α) {g : α → β} (hg : Antitone g) :
    g (⨅ i, f i) = ⨆ i, g (f i) :=
  map_iInf_of_monotone (β := βᵒᵈ) f hg

end Finite

[Michael Stoll]

OK; I think it is perhaps better to add these to my own PR (plus docs#MonotoneOn / docs#AntitoneOn versions).

[Snir Broshi]

Sure, can you also take the Monotone stuff from my PR?
(everything in ConditionallyCompleteLattice/Finset.lean, and ConditionallyCompleteLattice/Basic.lean below line 700)

[Snir Broshi]

Unless they're independent

[Michael Stoll]

I'll check, but it may take some time.

[Snir Broshi]

Hmm, perhaps I'll just split off that chunk to a separate PR?

[Snir Broshi]

#35822