Boolean sigma algebras and measure theory on them

Stream: general

[Pierre Quinton]

Hi everyone,

I am attempting to formalize my own thesis using Lean. It relates to Boolean sigma algebras, the countable chain condition, and measure theory on those. I realize that many things that I would have to do would fit nicely in mathlib, and therefore I think it makes sense to try to add them to the library.

I will follow roughly Halmos' "Introduction to Boolean algebras" and "Lectures on Boolean Algebras", but of course I will adapt things so that they fit nicely into mathlib.

I am rather new to Lean, so I am pretty sure I will need help often; I hope that is fine.

To start, I opened an issue: https://github.com/leanprover-community/mathlib4/issues/25849
The idea is that both inf_sSup_le_iSup_inf and iInf_sup_le_sup_sInf are provable, and therefore I have prepared a PR with that change. It consists essentially of moving those two statements out of CompleteBooleanAlgebra and making them into lemmas that we prove. Moreover, it removes the proof of those for every instance of CompleteBooleanAlgebra.

Any comments, or people interested, are welcome.

[Kevin Buzzard]

Please make a PR removing those fields, add the lemmas with the one-line proofs as mentioned in the issue and then see if you can fix up the library to get it all compiling again! The PR should mostly involve deleting code :-)

The way to make PRs to mathlib has recently changed, so searching this Zulip and maybe even some of the online docs might still be out of date (I don't know, all I know is that we are currently right in the middle of a big change). What you need to do is to fork mathlib, create a new branch, edit the file to remove the fields from the structure, and then try compiling locally with lake build and wait for 1 to 2 minutes. Probably other files will break; fix them. When the mathlib compilation process runs for a couple of minutes without any errors, try your luck: quit compiling locally (it will take an hour on a medium spec machine and you don't need to do this yourself) and make a PR to mathlib describing your change briefly. Then we'll see what CI says and you can ask again if it says something you don't understand.

[Pierre Quinton]

Thanks for the explanation, I tried my best following the guidelines (hopefully the new ones), here is the PR:
https://github.com/leanprover-community/mathlib4/pull/25909

I think it does exactly what you described, except that I made them theorem (it was not clear which it should be, but I can definitely change to lemma).

[Yaël Dillies]

FYI on Zulip you can type #25909 and it will render as #25909

[Kevin Buzzard]

@Pierre Quinton thanks a lot for your first merged PR!

[Pierre Quinton]

I have added a new PR (#25938) that follows the previous one. The idea is that since we do not have any more fields in CompleteBooleanAlgebra, we can now make CompleteAtomicBooleanAlgebra extend it directly. We also don't need anymore cast to CompleteBooleanAlgebra.

[Pierre Quinton]

I want to get working on Boolean sigma algebras. I can find no concepts related to Boolean sigma algebras, sigma Ideals, lattice that are closed under countable operations. The only remotely related material I could find are notions of Measurable sets which form sigma algebra without explicitly framing those as BooleanAlgebra (I might have missed something, obviously).

I am thinking of creating a new file BooleanSigmaAlgebra in Order (alternatively, we could group all BooleanAlgebra related material in a Order/BooleanAlgebra folder in a quick PR). In it, I am planning to add a class BooleanSigmaAlgebra (or maybe BooleanσAlgebra but this is slightly hard to read) that extends only BooleanAlgebra. I will then add some material to it, for instance I am thinking of duplicating a fair proportion of material from CompleteBooleanAlgebra as they share a lot of properties.

Alternatively, I am wondering about if there would be a way to change have an intermediate class that extends BooleanAlgebra and is given some constraint of type Set α → Prop which would typically be Set.Finite, Set.Countable or Set α → true. In this class, we could prove many of the properties that are currently in CompleteBooleanAlgebra. Then we would have that if it is constrained to Set.Finite, then it is a BooleanAlgebra, if it is constrained to Set.Countable, then it is a BooleanSigmaAlgebra and if it is Set α → true then it is CompleteBooleanAlgebra. I am not sure if My explanation makes sense, or if it is doable but I think it would be an interesting structure.

Any feedback would is most welcome, and I will provide update on my progress here.

[Pierre Quinton]

One possibility is the following:

import Mathlib.Order.BooleanAlgebra
import Mathlib.Order.Bounds.Defs
import Mathlib.Order.SetNotation
import Mathlib.Data.Set.Countable

universe u

variable {α : Type u}

class BooleanSigmaAlgebra (α) extends BooleanAlgebra α where

  /-- The supremum of a countable set. -/
  cSup (s : Set α) (hs : s.Countable) : α

  /-- The infimum of a countable set. -/
  cInf (s : Set α) (hs : s.Countable) : α


  /-- `cSup s hs` is a least upper bound of `s`. -/
  isLUB_cSup (s : Set α) (hs : s.Countable) : IsLUB s (cSup s hs)

  /-- `cInf s hs` is a greatest lower bound of `s`. -/
  isGLB_cInf (s : Set α) (hs : s.Countable) : IsGLB s (cInf s hs)

[Pierre Quinton]

Another possibility is this:

import Mathlib.Order.BooleanAlgebra
import Mathlib.Order.Bounds.Defs
import Mathlib.Order.SetNotation
import Mathlib.Data.Set.Countable

universe u

variable {α : Type u}


class BooleanSigmaAlgebra (α) extends BooleanAlgebra α where
  iSup (f : ℕ → α) : α
  iInf (f : ℕ → α) : α

  le_iSup (f : ℕ → α) (n : ℕ) : f n ≤ iSup f
  iSup_le (f : ℕ → α) (a : α) : (∀ n : ℕ, f n ≤ a) → iSup f ≤ a

  iInf_le (f : ℕ → α) (n : ℕ) : iInf f ≤ f n
  le_iInf (f : ℕ → α) (a : α) : (∀ n : ℕ, a ≤ f n) → a ≤ iInf f

For now I like this one better, it feels simpler. The only weird thing is that the iSup here is not related to SupSet in any kind of way.

[Yaël Dillies]

@Pierre Quinton, sorry for the delay, but both your ideas above will be impractical:

• They don't give you access to the existing ⨅/⨆ notations
• They have restricted inputs

[Yaël Dillies]

More subtly, your second definition doesn't give you the supremum/infimum of the empty set, so eg ℝ should be a boolean sigma algebra according to that definition actually no it wouldn't be, but something along those lines, eg ordinals should work

[Yaël Dillies]

I suggest instead you take in total functions sSup/sInf, and assert that they are LUBs/GLBs only if the given sets are countable. This would look like

class BooleanSigmaAlgebra (α) extends BooleanAlgebra α where
  sSup : Set α → α
  sInf : Set α → α
  isLUB_sSup (s : Set α) (hs : s.Countable) : IsLUB (sSup s) s
  isGLB_sInf (s : Set α) (hs : s.Countable) : IsGLB (sInf s) s

[Yaël Dillies]

Have fun!

[Pierre Quinton]

@Yaël Dillies Yes, I have realized that when trying to prove anything. But it looks like I can only get ⨆ if I extend SupSet which would then define sSup for all sets, not just those that are of restricted cardinality.

For your second point, you are completely right, this definition is terrible.

I think that your solution works, but I feel weird about having sSup defined on any set. But I guess this is just a symbol, it doesn't mean anything, so this is fine. thanks a lot, I will explore it now!

[Yaël Dillies]

Indeed I am making your sSup/sInf have junk values. This is the same reasoning behind 1 / 0 = 0 or √-1 = 0: Better make your functions total than requiring your users to prove that inputs are valid every time they call then function

[Pierre Quinton]

BTW, should I then extend SupSet and InfSet to get the sSup and sInf instead of declaring them?

[Yaël Dillies]

Yes! Doesn't change a huge lot over declaring the instance separately, but why not, it saves you a few lines

[Michael Rothgang]

Yaël Dillies said:

I suggest instead you take in total functions sSup/sInf, and assert that they are LUBs/GLBs only if the given sets are countable. This would look like

class BooleanSigmaAlgebra (α) extends BooleanAlgebra α where
  sSup : Set α → α
  sInf : Set α → α
  isLUB_sSup (s : Set α) (hs : s.Countable) : IsLUB (sSup s) s
  isGLB_sInf (s : Set α) (hs : s.Countable) : IsGLB (sInf s) s

Should s : Set α be implicit here?

[Yaël Dillies]

Doesn't matter, since I hope Pierre will write the lemmas _root_.isLUB_σsSup {s : Set α} (hs : s.Countable) : IsLUB (sSup s) s and alike :wink:

[Pierre Quinton]

@Yaël Dillies Not sure I understand that. How can we know that s is countable in this statement?

[Yaël Dillies]

Whoops, typo

[Pierre Quinton]

I really like the idea of having s implicit everywhere, it makes the writing so much lighter, thanks a lot @Michael Rothgang

[Pierre Quinton]

I'm making nice progress. Here is a sample as a trailer:

/-- `⊓` distributes over `⨆`. -/
theorem inf_σsSup_eq (hs : s.Countable) {a : α} :
    IsLUB {a ⊓ b | b ∈ s} (a ⊓ sSup s) :=
  gc_inf_himp.isLUB_l_image (isLUB_σsSup hs)

/-- `⊔` distributes over `⨅`. -/
theorem sup_σsInf_eq (hs : s.Countable) {a : α} :
    IsGLB {a ⊔ b | b ∈ s} (a ⊔ sInf s) :=
  gc_sdiff_sup.isGLB_u_image (isGLB_σsInf hs)

Still figuring out the structure. For iSup, is it fine if I make the assumption that I have countable index set? Here is what I have in mind:

variable [BooleanSigmaAlgebra α] [Countable ι] {s : Set α} {f : ι → α}

I feel slightly weird about assuming globally that ι is countable, but not s (I always give hs : s.Countable to my theorems and lemmas). Any input is most welcome.

[Yaël Dillies]

Pierre Quinton said:

For iSup, is it fine if I make the assumption that I have countable index set? Here is what I have in mind:

variable [BooleanSigmaAlgebra α] [Countable ι] {s : Set α} {f : ι → α}

I feel slightly weird about assuming globally that ι is countable, but not s (I always give hs : s.Countable to my theorems and lemmas)

Looks exactly how I would expect it

[Pierre Quinton]

The book "Introduction to Boolean algebra" by Halmos' has a lot of statement on a Boolean algebra of the form

If $\{ p_i \}$ is a family of elements in a Boolean algebra, then
\begin{align*}
\left( \bigwedge_i p_i \right)' = \bigvee_i p_i'
\end{align*}
The equations are to be interpreted in the sense that if either term exists, then so does the other term and the two are equal.

I really like such formulations, and I think it would translate nicely as the lemma (maybe the name should change)

theorem compl_GLB_LUB_compl {a : α} {s : Set α} : IsLUB s a ↔ IsGLB {bᶜ | b ∈ s} aᶜ :=
 sorry

It feels like this would help factorize a fair amount of code between CompleteBooleanAlgebra and my new BooleanσAlgebra. Also a lot of such results manipulating LUBs and GLBs would be very useful for proofs.

What do you think of that?

[Yaël Dillies]

Sure! Generally using IsLUB/IsGLB is an underused great idea

[Pierre Quinton]

I'm trying to add the following (and similar results) to BooleanAlgebra.lean:

theorem inf_LUB_iff {s : Set α} {a : α} (b : α) : IsLUB s a → IsLUB {b ⊓ c | c ∈ s} (b ⊓ a) := by
  exact gc_inf_himp.isLUB_l_image

But GaloisConnection.isLUB_l_image is defined in Mathlib.Order.GaloisConnection.Basic and the problem is that if I try to import it, I get a cyclic import. I am not sure why exactly, and I don't really know what is the appropriate way to proceed. Any help would be most welcome.

[Yaël Dillies]

The answer is that Order.GaloisConnection should be split into one file about preorders/partial orders/linear orders/lattices, one file about boolean algebras, one file about...

[Pierre Quinton]

Then should I move BooleanAlgebra related things from GaloisConnection to BooleanAlgebra.lean? Or should I make that a separate file?

[Yaël Dillies]

A new file under Order.BooleanAlgebra is probably best

[Pierre Quinton]

So mkdir BooleanAlgebra in Order? I guess this is a bit of refactor to make things a bit cleaner. How about the following files in it:

• Defs.lean
• Basic.lean
• InfiniteLaws.lean
• CompleteBooleanAlgebra lean

The last one would contain infinite laws on Boolean algebra and the only BooleanAlgebra related statement in GaloisConnection:

protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) :
    GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := fun a b ↦ by
  dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

[Yaël Dillies]

What's an infinite law?

[Pierre Quinton]

Pierre Quinton said:

I'm trying to add the following (and similar results) to BooleanAlgebra.lean:

theorem inf_LUB_iff {s : Set α} {a : α} (b : α) : IsLUB s a → IsLUB {b ⊓ c | c ∈ s} (b ⊓ a) := by
  exact gc_inf_himp.isLUB_l_image

But GaloisConnection.isLUB_l_image is defined in Mathlib.Order.GaloisConnection.Basic and the problem is that if I try to import it, I get a cyclic import. I am not sure why exactly, and I don't really know what is the appropriate way to proceed. Any help would be most welcome.

All the results of this form with LUBs and GLBs. I could also make that part of the Basic.lean

[Yaël Dillies]

CompleteBooleanAlgebra should probably not be under Order.BooleanAlgebra

[Filippo A. E. Nuccio]

Pinging @Sam van G who might be interested.

[Pierre Quinton]

I am a bit worried about backward compatibility on that. I want to avoid it as much as possible

[Pierre Quinton]

Actually, I just realized that the import problem comes from the import of BooleanAlgebra in Set.Basic with the following instance:

instance instBooleanAlgebra : BooleanAlgebra (Set α) :=
  { (inferInstance : BooleanAlgebra (α → Prop)) with
    sup := (· ∪ ·),
    le := (· ≤ ·),
    lt := fun s t => s ⊆ t ∧ ¬t ⊆ s,
    inf := (· ∩ ·),
    bot := ∅,
    compl := (·ᶜ),
    top := univ,
    sdiff := (· \ ·) }

Do you think there is a way to move that in BooleanAlgebra.lean?

[Yaël Dillies]

@Artie Khovanov was thinking about this

[Pierre Quinton]

For the original goal, I am planing on adding all of those (as soon as we fix this import issue):

-- This is true of a Lattice
theorem GLB_assoc {ss : ι → Set α} {a : α} (f : ι → α) (hss: ∀ i : ι, IsGLB (ss i) (f i)) :
    IsGLB {b : α | ∃ i : ι, b ∈ ss i} a ↔ IsGLB {f i | i : ι} a :=
  sorry

-- This is true of a Lattice
theorem LUB_assoc {ss : ι → Set α} {a : α} (f : ι → α) (hss: ∀ i : ι, IsLUB (ss i) (f i)) :
    IsLUB {b : α | ∃ i : ι, b ∈ ss i} a ↔ IsLUB {f i | i : ι} a :=
  sorry

theorem GLB_compl {s : Set α} {a : α} : IsLUB {bᶜ | b ∈ s} a ↔ IsGLB s aᶜ :=
  sorry

theorem LUB_compl {s : Set α} {a : α} : IsGLB {bᶜ | b ∈ s} a ↔ IsLUB s aᶜ :=
  sorry

theorem inf_LUB {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsLUB {b ⊓ c | c ∈ s} (b ⊓ a) :=
  gc_inf_himp.isLUB_l_image hs

theorem LUB_inf {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsLUB {c ⊓ b | c ∈ s} (a ⊓ b) :=
  sorry

theorem sup_GLB {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsGLB {b ⊔ c | c ∈ s} (b ⊔ a) :=
  gc_sdiff_sup.isGLB_u_image hs

theorem GLB_sup {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsGLB {c ⊔ b | c ∈ s} (a ⊔ b) :=
  sorry

theorem sdiff_LUB {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsGLB {b \ c | c ∈ s} (b \ a) :=
  sorry

theorem LUB_sdiff {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsLUB {c \ b | c ∈ s} (a \ b) :=
  sorry

theorem sdiff_GLB {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsLUB {b \ c | c ∈ s} (b \ a) :=
  sorry

theorem GLB_sdiff {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsGLB {c \ b | c ∈ s} (a \ b) :=
  sorry

theorem himp_LUB {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsLUB {b ⇨ c | c ∈ s} (b ⇨ a) :=
  sorry

theorem LUB_himp {s : Set α} {a : α} (b : α) (hs : IsLUB s a) : IsGLB {c ⇨ b | c ∈ s} (a ⇨ b) :=
  sorry

theorem himp_GLB {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsGLB {b ⇨ c | c ∈ s} (b ⇨ a) :=
  sorry

theorem GLB_himp {s : Set α} {a : α} (b : α) (hs : IsGLB s a) : IsLUB {c ⇨ b | c ∈ s} (a ⇨ b) :=
  sorry

I think they will be very practical for handling LUBs and GLBs and will make implementation of many things easier for CompleteBooleanAlgebra and BooleanSigmaAlgebra.

[Artie Khovanov]

You can split Set.Basic but tbh you probably end up duplicating API (i.e., proving facts once for set intersections and again for general joins)

[Pierre Quinton]

Actually, I think I can solve my cyclic import problem by simply splitting BooleanAlgebra into BooleanAlgebra.Basic and BooleanAlgebra.Defs. This is because I need the Set related import only for the proofs, and BooleanAlgebra is imported in Set.Basic only via the Defs.

Is there any guide I should follow for this type of structure? Should I duplicate the docstrings? Is there one package that is structured like that and is considered a good target?

[Kevin Buzzard]

This is the way that several other parts of mathlib are modelled so if it's a good fit for you then go for it! The module docstrings should probably be modified a bit, I would just duplicate the copyright headers unless you really want to go into the git history (which might involve going back to mathlib3 in this case, I can't remember) but the new module docstrings should reflect what's happening in the files. Any split PR like this (splitting a file) should be a one-off PR which does nothing else at all other than deleting the old files, creating the new files and modifying the module docstrings so that they're appropriate. This should then be followed up with a second PR tagged easy which deprecates the old file ie adds it back and just makes it import the new files and adds a deprecation line ensuring that anyone who tries to import it gets a warning rather than an error. For a reason I'm unclear about the preference of the community is currently to do this in a second PR.

[Kevin Buzzard]

I would prioritise this split if you're convinced that it's the way forward because this should be done as the first step of this refactor.

[Michael Rothgang]

The reason for preferring a split is cleaner history and diffs: a PR moving a 1000-line file, but adding the deprecation looks like a 900 line deletion plus a 1000 line addition. (Yes, you can diff things locally, but this is extra effort. And this occurs every time a future contributor wants to check.) If you just move a file, you get a sane diff.

[Michael Rothgang]

I should also add there there is work on automating the second part, i.e. auto-generating such PRs.

[Pierre Quinton]

This is what I tried to do in #26173 . I moved BooleanAlgebra.lean to BooleanAlgebra/Defs.lean, then I created BooleanAlgebra/Basic.lean and moved all theorems there, I also adapted the docstrings. I don't know if I could have done it better to keep the git authorship.
Let me know if this looks fine.

[Pierre Quinton]

I am now working on the deprecation/warning when I create the file. One way to do that would be to create a dummy theorem which is deprecated. Is that the standard way of doing that? Is there a known example somewhere I can copy?

[Aaron Liu]

You can copy file#Topology/GDelta/UniformSpace

[Pierre Quinton]

Done in #26176 , I cannot add the tag easy.

[Pierre Quinton]

Even if the tests were passing, I don't think that any of these PRs should be merged yet. I think they do not resolve the cyclic import problem. I am thinking about a solution, which could involve including part of the material that is currently in Basic into Defs to decrease the need to import BooleanAlgebra.Basic into other parts of mathlib.
If anyone has an idea on something I could try, I'm all ears.

[Kevin Buzzard]

Pierre Quinton said:

Done in #26176 , I cannot add the tag easy.

Oh apologies, this is the new regime now.

[Pierre Quinton]

Does anyone know what failed in #26176 ? the error is a bit cryptic: https://github.com/leanprover-community/mathlib4/actions/runs/15773295542/job/44462125321?pr=26176

If we fix it, then both #26173 and #26176 are ready.
I don't know if splitting a file in such Defs and Basic is generally a good idea, but I think it does not solve my problem as I may have to think the structure differently. So either we merge them or I will close them.

Regarding the structure, I was working on this idea of being able to work with LUBs and GLBs, trying to get nice arithmetic on them (you can find them at the end of the message). There are few things worth noticing:

• Most are not dependent on BooleanAlgebras but can most likely be proven from semi lattices and (co)heyting algebras
• I think that this idea of being able to work with limit operations on spaces that may not be closed under all such operations is more general than that. For instance, I was exploring LiminfLimsup and it looks like the problem is the same there, they are defined on Dedekind complete lattices (ConditionallyCompleteLattice) even though the inf, sup, liminf, limsup and lim (characterized by existence of liminf, limsup and their equality) might exist in any partially ordered set.
• The way I define theorems was an attempt at making their usage nice, e.g., from a proof that something is a LUB, you can prove that something else is a LUB. My hope was that this would lead to a nice way to chain them to obtain composite results, but in the end it was a pain to use them to prove anything, so I think we should do better than that.

Any idea/suggestion would be most welcome!

Here are the theorems:

/-
Copyright (c) 2025 Pierre Quinton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Pierre Quinton
-/
import Mathlib.Order.BooleanAlgebra.Basic
import Mathlib.Order.Bounds.Defs
import Mathlib.Order.GaloisConnection.Basic

universe u v

variable {α : Type u} [BooleanAlgebra α] {ι : Sort v} {s : Set α} {a : α} {b : α}

-- SemilatticeSup
theorem GLB_assoc {ss : ι → Set α} (f : ι → α) (hss: ∀ i : ι, IsGLB (ss i) (f i)) :
    IsGLB {b : α | ∃ i : ι, b ∈ ss i} a ↔ IsGLB {f i | i : ι} a :=
  sorry

-- SemilatticeInf
theorem LUB_assoc {ss : ι → Set α} (f : ι → α) (hss: ∀ i : ι, IsLUB (ss i) (f i)) :
    IsLUB {b : α | ∃ i : ι, b ∈ ss i} a ↔ IsLUB {f i | i : ι} a :=
  sorry

-- BooleanAlgebra possibly HeytingAlgebra
theorem GLB_compl : IsLUB {bᶜ | b ∈ s} a ↔ IsGLB s aᶜ := by
  sorry

-- BooleanAlgebra possibly CoheytingAlgebra
theorem LUB_compl : IsGLB {￢b | b ∈ s} a ↔ IsLUB s (￢a) :=
  sorry

-- HeytingAlgebra
theorem inf_LUB (hs : IsLUB s a) : IsLUB {b ⊓ c | c ∈ s} (b ⊓ a) :=
  gc_inf_himp.isLUB_l_image hs

-- HeytingAlgebra
theorem LUB_inf (hs : IsLUB s a) : IsLUB {c ⊓ b | c ∈ s} (a ⊓ b) := by
  simp_rw [inf_comm _ b]
  exact inf_LUB hs

-- CoheytingAlgebra
theorem sup_GLB (hs : IsGLB s a) : IsGLB {b ⊔ c | c ∈ s} (b ⊔ a) :=
  gc_sdiff_sup.isGLB_u_image hs

-- CoheytingAlgebra
theorem GLB_sup (hs : IsGLB s a) : IsGLB {c ⊔ b | c ∈ s} (a ⊔ b) := by
  simp_rw [sup_comm _ b]
  exact sup_GLB hs

theorem sdiff_LUB (hs : IsLUB s a) : IsGLB {b \ c | c ∈ s} (b \ a) :=
  sorry

-- CoheytingAlgebra
theorem LUB_sdiff (hs : IsLUB s a) : IsLUB {c \ b | c ∈ s} (a \ b) :=
  gc_sdiff_sup.isLUB_l_image hs

theorem sdiff_GLB (hs : IsGLB s a) : IsLUB {b \ c | c ∈ s} (b \ a) :=
  sorry

theorem GLB_sdiff (hs : IsGLB s a) : IsGLB {c \ b | c ∈ s} (a \ b) :=
  sorry

theorem himp_LUB (hs : IsLUB s a) : IsLUB {b ⇨ c | c ∈ s} (b ⇨ a) :=
  sorry

theorem LUB_himp (hs : IsLUB s a) : IsGLB {c ⇨ b | c ∈ s} (a ⇨ b) :=
  sorry

theorem himp_GLB (hs : IsGLB s a) : IsGLB {b ⇨ c | c ∈ s} (b ⇨ a) :=
  gc_inf_himp.isGLB_u_image hs

theorem GLB_himp (hs : IsGLB s a) : IsLUB {c ⇨ b | c ∈ s} (a ⇨ b) :=
  sorry

example (hs : IsGLB s a) : IsLUB {cᶜ ⊓ (b ⊔ a) | c ∈ s} (aᶜ ⊓ (b ⊔ a)) := by
  apply LUB_inf (LUB_compl hs)

[Aaron Liu]

The problem is that you added new files. You need to run the command lake exe mk_all to regenerate the import all files.

[Pierre Quinton]

I have opened a PR (#26318) to add BooleanσAlgebra. For now it just provides the definition of BooleanσAlgebra and some instances. I tried to make every commit very atomic so that it is easy to review. I think that we can already probably improve both instances, my implementation might be inefficient.

My plan is then to mimic a lot of results from ConditionallyCompleteLattice and CompleteBooleanAlgebra and add them in Basic.lean.

Any comment or idea is most welcome.

EDIT: Also, should I do everything in one PR as this is starting a new concept (to see if we do want to merge it in the end), or should I cut in smaller PRs (because we know we will eventually do it)?

[Pierre Quinton]

Between the two proofs of the second theorem:

theorem σSup_le_iff (hs : s.Countable) : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  isLUB_le_iff (isLUB_σsSup hs)

theorem le_σsInf_iff (hs : s.Countable) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b :=
  -- le_isGLB_iff (isGLB_σsInf hs)
  σSup_le_iff (α := αᵒᵈ) hs

There seems to be a tendency in Mathlib to prefer the first one (i.e. not the one by duality). Is there a good reason for that? It is tempting to state all dual proofs as such.

[Aaron Liu]

To do the proof by duality you have to import duality

[Pierre Quinton]

In ConditionallyCompleteLattice, there is this result:

/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness above for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem lt_csSup_of_lt (hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s :=
  lt_of_lt_of_le h (le_csSup hs ha)

I think that in the case of a Boolean sigma algebra, conditioned on countability of s, this is supposed to be an equivalence, like for complete lattices. I could not find the corresponding result in CompleteLattice, does that ring a bell to anyone?

[Pierre Quinton]

Well, I think it is essentially this:

theorem lt_isLUB_iff (h : IsLUB s a) : b < a ↔ ∃ c ∈ s, b < c

EDIT:
Actually this holds only in linear orders. In a Boolean algebra, it doesn't hold:
If we have x, y and z, and we let s={x, y, z} as well as b = x ⊔ y, then we can have b < a while ∃ c ∈ s, b < c would be false.

[Pierre Quinton]

Little update: I have introduced the intermediary concept of SigmaCompleteLattice to decompose better the responsabilities and match the structure of CompleteBooleanAlgebra.

I also have the following question: In some cases, for a set s, there is a LUB. I think that in that case, we want sSup s to be that LUB. As an example, if (h : IsGreatest s a), then a is the LUB of s, and we would like sSup s to equal a. I am therefore wondering about adding two statements to SigmaCompleteLattice:

  isLUB_sSup_of_isLUB (a : α) (s : Set α) (h : IsLUB s a) : IsLUB s (sSup s)
  isGLB_sInf_of_isGLB (a : α) (s : Set α) (h : IsGLB s a) : IsGLB s (sInf s)

Is this the good way to proceed? Are the name correct? I didn't put the σ here as this is not related to countability. So the over SigmaCompleteLattice would be defined as

class SigmaCompleteLattice (α) extends Lattice α, SupSet α, InfSet α where
  isLUB_σsSup (s : Set α) (hs : s.Countable) : IsLUB s (sSup s)
  isGLB_σsInf (s : Set α) (hs : s.Countable) : IsGLB s (sInf s)

  isLUB_sSup_of_isLUB (a : α) (s : Set α) (h : IsLUB s a) : IsLUB s (sSup s)
  isGLB_sInf_of_isGLB (a : α) (s : Set α) (h : IsGLB s a) : IsGLB s (sInf s)

[Pierre Quinton]

I have a question that is a bit more general than the scope of this project.

The type classes SupSet α and InfSet α define respectively the mapping sSup : Set α → α and sInf : Set α → α. The role of those mapping is to represent the suprema and infima of sets.
I am wondering why this is not enforced by any property. For instance, I think it would make sense to have statement stating that if there exists a LUB a on a set s, then sSup s = a.
This would effectively enforce that if s has a supremum, then this supremum is sSup. Now if we think for instance of a CompleteLattice, then we only need to ensure that every set s has a LUB, and then this LUB is sSup.
In CompleteLattice or in ConditionallyCompleteLattice, it doesn't make any difference as in the former, every suprema exist and in the later, they exists if and only if the set is bounded above and non-empty.
In my case (SigmaCompleteLattice), I want to have a statement saying that the supremum of every countable set exists, but of course there could be many other set with some supremum (for instance, if a is the greatest element of s).
For a Lattice, we could then prove that the infima and suprema of every finite collection exists and is sSup and sInf.

Note that this formalism would also make it possible to have the functions sSup and sInf defined on PartialOrder, and in principle, we could prove some statement with them. For instance, on a BooleanAlgebra, we could prove
then

theorem inf_sSup_le_iSup_inf (a : α) {s : Set α} (hs : ∃ b : α, IsLUB s b) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

which states that ⊓ distributes over ⨆. Actually, I think we would also want a proof that a ⊓ sSup s is the LUB of {a ⊓ b | b ∈ s}.
Anyways, I am not sure if this is a good idea or if there was very specific to not have that, let me know if this makes (no) sense. I have attempted a structure for that:

variable {α : Type*}

class OrderSupSet (α) extends PartialOrder α, SupSet α where
  isLUB_sSup {s : Set α} (a : α) (hs : IsLUB s a) : IsLUB s (sSup s)

class OrderInfSet (α) extends PartialOrder α, InfSet α where
  isGLB_sInf {s : Set α} (a : α) (hs : IsGLB s a) : IsGLB s (sInf s)

instance (priority := 100) PartialOrder.toOrderSupSet [PartialOrder α] :
    OrderSupSet α where
  sSup s :=
    if h : ∃ a, IsLUB s a then Classical.choose h
    else Classical.arbitrary α
  isLUB_sSup {s} hs := by
    sorry

instance (priority := 100) PartialOrder.toOrderInfSet [PartialOrder α] :
    OrderInfSet α where
  sInf s :=
    if h : ∃ a, IsGLB s a then Classical.choose h
    else Classical.arbitrary α
  isGLB_sInf {s} hs := by
    sorry

The last instance doesn't work (I am not used to working with choice), but I think it provides the intuition.

[Aaron Liu]

Pierre Quinton said:

Anyways, I am not sure if this is a good idea or if there was very specific to not have that, let me know if this makes (no) sense.

I am also not sure this is a good idea, do you have any specific use cases in mind?

[Pierre Quinton]

I think it separates better where the results come from. Some results are essentially always, an example is:

theorem IsGreatest.csSup_eq (H : IsGreatest s a) : sSup s = a

In ConditionallyCompleteLattice. In SigmaCompleteLattice, such a result cannot be proven as sSup cannot be proven to be the supremum of s unless s is countable, but clearly here, s has a greatest element and therefore has a LUB, its just that this LUB is not provably sSup s.

I think that some fair proportion of results of CompleteLattice and ConditionallyCompleteLattice can be factored as results on lattice with this structure.

Later, I would also like to add the countable chain condition in combination with BooleanSigmaAlgebra. It states that any anti-chain is a most countable. This implies that the Boolean algebra is actually complete.

In general, a structure that would factor results from CompleteLattice, ConditionallyCompleteLattice and SigmaCompleteLattice would feel less like repeating every statement three times, I think it would then typically reduce the probability of forgetting to change all three when we change one. Finally it satisfies a bit more the single responsibility principle. It would be weird to add such a structure to SigmaCompleteLattice even though it has nothing to do with sigma completeness.

[Aaron Liu]

Pierre Quinton said:

In general, a structure that would factor results from CompleteLattice, ConditionallyCompleteLattice and SigmaCompleteLattice would feel less like repeating every statement three times, I think it would then typically reduce the probability of forgetting to change all three when we change one.

That's what IsGLB and IsLUB are for, right?

[Pierre Quinton]

Yes but in SupSet, it is said:

sSup s is the supremum of the set s;

But this is not true if I only guarantee that sSup s is the supremum of s whenever s is countable. So it feels like we also want to guarantee that sSup s is the supremum of s whenever there is a such that IsLUB s a, right?

[Pierre Quinton]

Alright, I think I will try to push BooleanSigmaAlgebra and SigmaCompleteLattice as much as possible without this structure. If I get to some unconfortable things later, it will provide material to think about these things. I am therefore removing this from SigmaCompleteLattice in #26318

[Pierre Quinton]

Does any know a short proof that if (hs : s.Countable), then (s ∩ t).Countable?

[Aaron Liu]

Pierre Quinton said:

Does any know a short proof that if (hs : s.Countable), then (s ∩ t).Countable?

docs#Set.Countable.mono along with docs#Set.inter_subset_left

[Pierre Quinton]

Thank, I ended up using mono and simp

[Pierre Quinton]

In https://github.com/leanprover-community/mathlib4/pull/26318/commits/4e926313a0984ab289e43e4d4a40a850b1699b1d I have added a lot of theorems about iSup and iInf. I would appreciate some review, in particular on the countability assumptions that I make and if they make sense:

variable [SigmaCompleteLattice α] {s t : Set α} {a b : α}
[Countable ι] [Countable ι'] [∀ j, Countable (κ j)] [∀ j, Countable (κ' j)] {f g : ι → α} {i : ι}

[Pierre Quinton]

The reason I am asking about my assumptions for the iSup/iInf theorems is that I am struggling with a proof which should probably easier. I have introduce this theorem

theorem σsSup_eq_σiSup (hs : s.Countable) : sSup s = ⨆ a ∈ s, a :=
  le_antisymm (σsSup_le hs le_σiSup₂) (σiSup₂_le fun _ => le_σsSup)

And the proof doesn't work, I am supposed to prove that α is countable which it might not be for le_σiSup₂. This proof is adapted from the corresponding theorem in CompleteLattice:

theorem sSup_eq_iSup {s : Set α} : sSup s = ⨆ a ∈ s, a :=
  le_antisymm (sSup_le le_iSup₂) (iSup₂_le fun _ => le_sSup)

The prototype is

theorem le_σiSup₂ [SigmaCompleteLattice α] [Countable ι] [∀ j, Countable (κ j)]  {f : ∀ i, κ i → α} (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j

And in the application I want to have, I think that ι is supposed to be α and κ i is i ∈ s. Therefore there are uncountably many element in the iSup, but only countably many of those are different. I am not sure what I should do to my assumption to fix that, I guess this is only about all the theorems involving σiSup₂ and σiInf₂

[Yaël Dillies]

Hey Pierre, your PR and this thread are still on my radar, but I am still under the weather. You should receive a review from me in the next week or so

[Pierre Quinton]

Thanks, there is no rush, I will provide updates here on my progress and anyways there are many other things to do (I just have proven theorems about SigmaCompleteLattice but none about BooleanSigmaAlgebra), so take your time!

[Kevin Buzzard]

Pierre did you already get warned about this gotcha ? I wonder whether it affects you here. Maybe you want to just write ⨆ a : s, a to avoid this?

[Pierre Quinton]

@Kevin Buzzard I was totally unaware of this, and somehow, I think this unblocked me quite a lot.

Still, I think that ⨆ a ∈ s, a should exist whenever s.Countable holds (currently it is not, but I think there might be a way):
Note that ⨆ a ∈ s, a is shorthand for ⨆ (a : α), ⨆ (_ : a ∈ s), a. For each a not in s, {a | ∃ _ : a ∈ s} is empty (and therefore countable) and therefore ⨆ (_ : a ∈ s), a equals ⊥. On the other hand, if a is in s, then {a | ∃ _ : a ∈ s}={a} (which is countable) and so ⨆ (_ : a ∈ s), a = a. Now if we write f (a : α) to be a if a is in s and ⊥, then {f a | a : α} is contained in the union of s and {⊥}, which is therefore countable, so the iSup should exist.

This hints that we should have a version of the iSup theorems based on the countability of the image of f instead.

If that sounds reasonable to you, I will go for that!

[Kevin Buzzard]

Aah yes, if there is a sensible answer for sup(empty set) then the gotcha won't apply to you (which is a relief).

[Pierre Quinton]

Well, for sure in a BooleanSigmaAlgebra there should be, but also, as the empty set is countable, it should have sSup and sInf, so those better be bot and top. It indicates that SigmaCompleteLattice should be a BoundedOrder. BTW, do you know any reason why CompleteLattice reimplements the structure of BoundedOrder instead of extending it? Is there any reason I should do the same?

[Pierre Quinton]

Actually, I think that it is wrong (or rather inefficient) to assume in CompleteLattice the following:

  /-- Any element is less than the top one. -/
  protected le_top : ∀ x : α, x ≤ ⊤
  /-- Any element is more than the bottom one. -/
  protected bot_le : ∀ x : α, ⊥ ≤ x

Ina CompleteLattice, we can show that there exists a minimal element. For instance, we can use the GLB of the empty set and show that it is smaller than any element because of monotonicity of sSup applied to ∅ and any singleton {a}. We could then have an instance of BoundedOrder instead of assuming it. The exact same reasoning works for me as all involved sets are countable.

My solution is the following:

instance (priority := 100) SigmaCompleteLattice.toBoundedOrder [SigmaCompleteLattice α] :
    BoundedOrder α where
  top := sInf ∅
  bot := sSup ∅
  le_top (a : α) := isGLB_empty_iff.1 (isGLB_σsInf ∅ Set.countable_empty) a
  bot_le (a : α) := isLUB_empty_iff.1 (isLUB_σsSup ∅ Set.countable_empty) a

Which seems to work, I have made a PR (#26574) with the same change to CompleteLattice. This introduced some errors that I struggle fixing, any help would be welcome.

[Pierre Quinton]

(deleted)

[Kevin Buzzard]

I don't know much about this corner of the library and am hoping that someone who does will chime in, but my guess is that the way it's set up the way it is is to give people more flexibility in choosing their bottom and top elements up to definitional equality, and that the change you're suggesting will not be desired because it removes this. In other words this is not a mathematical decision but a CS-related one. Your suggestion is making the typeclass system conjure data out of nowhere and definitional equality matters when it comes to data in the typeclass system.

[Kevin Buzzard]

In other words, there are probably plenty of situations where although it might be a theorem that top = sInf empty, it might be very annoying (or even unworkable in practice) to have this as the definition of top, in your favourite complete lattice.

[Pierre Quinton]

I guess this is a synctatic choice rather than a semantic one? But still, it feels weird to constrain the definition of CompleteLattice because some type classes that extend it want to define their own top and bot. It feels like it should be the responsability of things that are CompleteLattices to define their top and bot element differently if they want. For instance, the powerset of X need not extend CompleteAlgebra if we want top to be X and bot to be the emptyset, it can then provide an instance of CompleteLattice and also some theorems to prove that the top and bot elements are really X and emptyset. I'm guessing the problem with that would be that we would have to use those theorems a lot, or even replicate most theorems about them?

[Yaël Dillies]

Yes, exactly. The top and bot fields are here to stay

[Kenny Lau]

@Pierre Quinton the real way to solve it is to make a custom constructor rather than changing the definition, because we sometimes definitely want a top/bot that is defeq to something and not defined to be the Inf/Sup of the empty set

[Kenny Lau]

for example, in ideals, bot is defeq to {x | x = 0}

[Pierre Quinton]

I think I'm starting to get it, however I have one last question. If we take ideals for instance, we don't we have sSup ∅={x | x = 0}? Because if we did, then setting bot to sSup ∅ would work right?

[Aaron Liu]

We do have sSup ∅ = {x | x = 0}, but it's not a definitional equality

[Pierre Quinton]

It feels like I am mixing several levels of abstraction, sorry about that.

[Aaron Liu]

Definitional equality is when things are equal "by definition"

[Aaron Liu]

Do you know what definitional equality is? I can explain it a bit more if you want.

[Pierre Quinton]

I think I am fine (after some reading). It is just not clear that I should do the same for SigmaCompleteLattices. For instance a sigma algebra is a SigmaCompleteLattice and I want to top to be the full set and the bot to be the empty set, so the problem seems to be the same.

[Aaron Liu]

Let's say you define an instance of CompleteLattice on WithTop Nat.

[Aaron Liu]

Then coming from ∀ α, Top (WithTop α) you get a top

[Aaron Liu]

and coming from CompleteLattice (WithTop Nat) you get another top

[Aaron Liu]

It's bad if they're not definitionally equal because then you can have goal like ⊤ = ⊤ that's not rfl because the tops are coming from different instances

[Kenny Lau]

@Pierre Quinton It's not clear to me that you understand what defeq means

[Aaron Liu]

So we add a top field to CompleteLattice so that instead of the instance filling in top := sInf ∅ for you, you can make it be the same one coming from ∀ α, Top (WithTop α) instead (but then you have to prove it's the same top)

[Aaron Liu]

And if you want to fill in everything automatically you can still use docs#completeLatticeOfCompleteSemilatticeSup and docs#completeLatticeOfCompleteSemilatticeInf

[Aaron Liu]

This is the same reason we have copies like docs#Units.copy and docs#RingHom.copy

[Pierre Quinton]

Aaron Liu said:

It's bad if they're not definitionally equal because then you can have goal like ⊤ = ⊤ that's not rfl because the tops are coming from different instances

Alright, this made it very clear.

[Pierre Quinton]

[Quoting…]

Yes, I was not clear with this, sorry about that.

[Kenny Lau]

@Pierre Quinton you need to pay attention when replacing data. replacing proofs is fine because of proof irrelevance, but for data we care about defeq

[Kenny Lau]

in fact we recently just had a refactor on complete lattices? does anyone remember which PR that was?

[Kenny Lau]

@Aaron Liu do you remember?

[Aaron Liu]

I could take a look at complete lattice code and see the blame

[Aaron Liu]

but I don't remember

[Aaron Liu]

I found #23064 is this the one you're thinking of

[Pierre Quinton]

Aaron Liu said:

Let's say you define an instance of CompleteLattice on WithTop Nat.

Going back to this example, why doesn't lean require in this case to prove that the two defeq for tops are the same? Because it feels like when we view α as a WithTop Nat, we want the top to be defeq to the meaningfull top while when viewing α as a CompleteLattice, we could want that top to be defeq to sInf ∅. In a sense it still feels to me that the defeq of a type depends on the level of abstraction that we consider.

Also, is there any reason that CompleteLattice does not extend BoundedOrder instead of defining le_top and bot_le?

[Aaron Liu]

You can't prove things are defeq in Lean

[Aaron Liu]

Pierre Quinton said:

Also, is there any reason that CompleteLattice does not extend BoundedOrder instead of defining le_top and bot_le?

I have no idea

[Kenny Lau]

@Pierre Quinton it still really seems like you don't understand defeqs, lemme try to come up with an example for you to play with...

[Kenny Lau]

but before that, @Aaron Liu @Pierre Quinton I found the PR I was talking about: #25909 changed:

class CompleteBooleanAlgebra (α) extends CompleteLattice α, BooleanAlgebra α where
  /-- `⊓` distributes over `⨆`. -/
  inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
  /-- `⊔` distributes over `⨅`. -/
  iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

to:

class CompleteBooleanAlgebra (α) extends CompleteLattice α, BooleanAlgebra α

because it turned out that the two axioms required were actually provable! and this does not create any issues, because we're replacing theorems rather than data

[Kenny Lau]

universe u

@[ext]
class Bot (α : Type u) where
  bot : α

notation "⊥" => Bot.bot

#check NatCast

class CanonicalNatCast (α : Type u) extends NatCast α, Bot α where
  bot_eq_zero : (⊥ : α) = ↑(0 : Nat)

example {α : Type u} [CanonicalNatCast α] : (⊥ : α) = ↑(0 : Nat) := rfl -- fails!
example {α : Type u} [CanonicalNatCast α] : (⊥ : α) = ⊥ := rfl -- succeeds!

instance : CanonicalNatCast (Nat → Prop) where
  natCast n x := x < n -- n ↦ { x | x < n }
  bot x := False -- ⊥ := ∅ := { x | False }
  bot_eq_zero := funext fun x ↦ (eq_false <| Nat.not_lt_zero x).symm

#check (rfl : (⊥ : Nat → Prop) = ⊥) -- works!
#check (rfl : (⊥ : Nat → Prop) = ↑(0 : Nat)) -- fails!

/-- This is the function you propose, which is bad. -/
def NatCast.toCanonical (α : Type u) [NatCast α] : CanonicalNatCast α where
  bot := ↑(0 : Nat)
  bot_eq_zero := rfl

-- attribute [instance] NatCast.toCanonical

theorem diamond! : (⊥ : Nat → Prop) =
    @Bot.bot (Nat → Prop) (CanonicalNatCast.toBot (self := NatCast.toCanonical _)) := by
  -- ⊢ ⊥ = ⊥
  rfl -- doesn't work!

[Pierre Quinton]

Ah yeah, I did that one!

[Kenny Lau]

@Pierre Quinton here's your example to play with

[Kenny Lau]

so, lemme explain in words

[Kenny Lau]

CanonicalNatCast means that there's a way to cast a natural number to the type, and that 0 is mapped to the bottom element

[Kenny Lau]

and our toy example here is Nat -> Prop, which means (Set ℕ) (I didn't import Mathlib so I don't have those notations)

[Kenny Lau]

the way to cast the natural number n is to map it to { x | x < n }

[Kenny Lau]

so 37 is mapped to {0, 1, 2, ..., 36}

[Kenny Lau]

and naturally there's a bottom element, which is the empty set!

[Kenny Lau]

if you try removing the Bot from the requirement (as you reasoned, "obviously I can just set bot to be f 0!"), then you'll get a diamond

[Kenny Lau]

(there should technically be a way to tweak my code to make them defeq, and this is left as an exercise to the reader :upside_down: )

[Pierre Quinton]

Thanks a lot for the example, it helps. Actually my question was more about Lean itself than about Mathlib, so it shouldn't be asked here.

[Pierre Quinton]

@Kenny Lau Actually, another instance of exactly that problem is the fact that we could in principle define a CompleteLattice via only the infimums and deduce the supremum, but instead we define both and we can use https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/CompleteLattice/Defs.html#completeLatticeOfInf to do that if really needed. This completely answers my question because if we need the defeq of sup to be the one defined by an InfSet, then we could use (completeLatticeOfInf [...]).sSup.
So I will do exactly the same thing for SigmaCompleteLattice.

[Pierre Quinton]

Coming back to the problem with iSup2 I had, I am thinking of doing the following:

theorem σiSup₂_le {f : ∀ i, κ i → α} (hf₁ : ∀ i, (Set.range (f i)).Countable)
    (hf₂ : {iSup (f i) | i}.Countable) (h : ∀ i j, f i j ≤ a) : ⨆ (i) (j), f i j ≤ a :=
  σiSup_le hf₂ fun i => σiSup_le (hf₁ i) <| h i

This works, but maybe (hf₂ : {iSup (f i) | i}.Countable) is not the cleanest way of assuming that there are at most countably iSups.

[Pierre Quinton]

I made CompleteLattice extend BoundedOrder in #26626 in case that is a good idea.

[Kenny Lau]

@Pierre Quinton hmm, I don't immediately know why they didn't do that, let's see what others say

[Pierre Quinton]

Now that I have these:

variable {f g : ι → α} [Countable (Set.range f)] [Countable (Set.range g)] {i : ι}

-- ...

lemma σiSup_le (h : ∀ i, f i ≤ a) : ⨆ i, f i ≤ a

I want to prove the following lemma:

theorem σiSup₂_le {f : ∀ i, κ i → α} (hf₁ : ∀ i, (Set.range (f i)).Countable)
    (hf₂ : {iSup (f i) | i}.Countable) (h : ∀ i j, f i j ≤ a) : ⨆ (i) (j), f i j ≤ a :=
  haveI : Countable ↑(Set.range fun i ↦ ⨆ j, f i j) := hf₂
  σiSup_le fun i =>
    haveI : Countable ↑(Set.range (f i)) := hf₁ i
    σiSup_le <| h i

The proof I provide is valid, but I feel like it is very inefficient, does any one have an idea on how to improve on it?

Same question for this one:

theorem le_σiSup₂ {f : ∀ i, κ i → α} (hf₁ : ∀ i, (Set.range (f i)).Countable)
    (hf₂ : {iSup (f i) | i}.Countable) (i : ι) (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
  haveI : Countable ↑(Set.range fun i ↦ ⨆ j, f i j) := hf₂
  haveI : Countable ↑(Set.range (f i)) := hf₁ i
  le_σiSup_of_le i <| le_σiSup j

[Pierre Quinton]

I have managed to fix the few problems that I had. I think this is already a pretty big PR and I did not start with BooleanSigmaAlgebra specific results yet, I have only ported results from CompleteLattice and ConditionallycompleteLattice to SigmaCompleteLattice. I am wondering if we should aim for a merge with the current results and add results specific to BooleanSigmaAlgebras in another PR.

In the meantime, I would appreciate some review on the assumptions and proofs of all theorems that involves σiSup₂. It feels like my assumptions are pretty heavy and I don't know how we could make all this lighter, for instance:
https://github.com/leanprover-community/mathlib4/pull/26318/files#diff-f7ca657929701ee4af7c14463fef9035e3528d414ccafda2402b82f24dd633adR85

[Pierre Quinton]

To make working with statement involving ⨆ (i : ι) (j : κ i), f i j, I thought of assuming [Countable (Σ i, κ i)]. Note that as there are at most Countably many nonempty κ i and each of those have at most countably many elements, then we should be fine for the proofs in principle.

The usage of Sigma involves typing {ι : Type*} {κ : ι → Type*} and Type* excludes Prop which would be very useful to have. We could work with PSigma but I think it would make everything complicated.

I think this matter is a bit out of my skill set in Lean. Consider the illustration of the problem:

example (hs : s.Countable) : Countable (Sigma s) := sorry
example (hs : s.Countable) : Countable (PSigma s) := sorry

instance [Countable (Sigma κ)] : Countable (κ i) := sigma_mk_injective.countable
instance [Countable (PSigma κ)] : Countable (κ i) := sorry

example [Countable (Sigma κ)] : Countable (Sigma (Nonempty ∘ κ)) := sorry
example [Countable (PSigma κ)] : Countable (PSigma (Nonempty ∘ κ)) := sorry

example [Countable (Sigma κ)] {f : ∀ i, κ i → α} : {⨆ j, f i j | i : ι} := sorry
example [Countable (PSigma κ)] {f : ∀ i, κ i → α} : {⨆ j, f i j | i : ι} := sorry

The first and fifth statements fail with a type error as Prop is not a Type but a Sort would work. The PSigma variant are valid, and they would work with {ι : Sort*} {κ : ι → Sort*} (instead of Type*), however in the documentation, it is said:

In practice, this generality leads to universe level constraints that are difficult to solve, so PSigma is rarely used in manually-written code. It is usually only used in automation that constructs pairs of arbitrary types.

I am therefore worried that it will be very hard to prove statements involving PSigmas (and when I tried, it was indeed rather difficult).