Skip to content

chore(ConditionallyCompleteLattice/Indexed): dualize #38938

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lua-vr wants to merge 3 commits into
base: master
Choose a base branch
from
+94 −260
Open

chore(ConditionallyCompleteLattice/Indexed): dualize #38938

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
85654c3
chore: dualize ConditionallyCompleteLattice/Indexed
lua-vr May 4, 2026
271a91c
merge upstream
lua-vr May 31, 2026
e19202a
fixes
lua-vr May 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 30 additions & 69 deletions Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,23 +46,18 @@ Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot
variable [Preorder α]

open Classical in
@[to_dual]
noncomputable instance WithTop.instSupSet [SupSet α] :

@JovanGerb JovanGerb May 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
noncomputable instance WithTop.instSupSet [SupSet α] :
noncomputable instance [SupSet α] :

Can you put the first part of the file inside a namespace WithTop? Then you can also omit the name of the instance altogether.

That does require dualizing all of the declarations in the section.

SupSet (WithTop α) :=
⟨fun S =>
if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then
↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩

open Classical in
@[to_dual]
noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩

noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩

noncomputable instance WithBot.instInfSet [InfSet α] :
InfSet (WithBot α) :=
⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩

theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)

@JovanGerb JovanGerb May 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reason not to tag this with to_dual?

(hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
(if_neg hs).trans <| if_pos hs'
Expand All @@ -79,10 +74,11 @@ theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥})
sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
WithTop.sInf_eq (α := αᵒᵈ) hs h's

@[simp]
@[to_dual (attr := simp)]
theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
if_pos <| by simp

@[to_dual (attr := norm_cast)]

@lua-vr lua-vr May 4, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Was there a particular reason for the WithTop ones to not have norm_cast? With this PR, both versions get tagged for norm_cast

@JovanGerb JovanGerb May 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, this is probably an oversight. I'm not sure that this is actually a good norm_cast lemma. can you try removing the tag? If something breaks as a result, then we'll know why we need the norm_cast tag.

theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
classical
Expand All @@ -95,6 +91,7 @@ theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddB
· rw [preimage_image_eq]
exact Option.some_injective _

@[to_dual (attr := norm_cast)]
theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
classical
Expand All @@ -103,24 +100,10 @@ theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
· exact Option.some_injective _
· rintro ⟨x, _, ⟨⟩⟩

@[simp]
theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
WithTop.sInf_empty (α := αᵒᵈ)

theorem WithBot.sInf_empty (α : Type*) [CompleteLattice α] : (sInf ∅ : WithBot α) = ⊤ := by
rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
WithBot.coe_top]

@[norm_cast]
theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
WithTop.coe_sInf' (α := αᵒᵈ) hs h's

@[norm_cast]
theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
WithTop.coe_sSup' (α := αᵒᵈ) hs

end

instance ConditionallyCompleteLinearOrder.toLinearOrder [h : ConditionallyCompleteLinearOrder α] :
Expand Down Expand Up @@ -253,35 +236,29 @@ theorem notMem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove
/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w<b`.
See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt /-- Introduction rule to prove that `b` is
the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this
is not the case of any `w>b`. See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in
complete lattices. -/]
Comment on lines +239 to +242

@JovanGerb JovanGerb May 31, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt /-- Introduction rule to prove that `b` is
the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this
is not the case of any `w>b`. See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in
complete lattices. -/]
@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt
/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/]

I prefer starting the dual comment on a new line if it takes multiple lines, so that it aligns nicely with original comment. This makes it easier to edit both, and to ensure that they actually align. Similarly below

theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b)
(H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
(eq_of_le_of_not_lt (csSup_le hs H)) fun hb =>
let ⟨_, ha, ha'⟩ := H' _ hb
lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha

/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)

/-- `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. -/
@[to_dual csInf_lt_of_lt /-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when
`s` is bounded below. This is essentially an iff, except that the assumptions for the two
implications are slightly different (one needs boundedness below 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)

/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness below for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem csInf_lt_of_lt : BddBelow s → a ∈ s → a < b → sInf s < b :=
lt_csSup_of_lt (α := αᵒᵈ)

/-- If all elements of a nonempty set `s` are less than or equal to all elements
of a nonempty set `t`, then there exists an element between these sets. -/
theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty)
Expand Down Expand Up @@ -390,49 +367,38 @@ variable [ConditionallyCompleteLinearOrder α] {f : ι → α} {s : Set α} {a b

/-- When `b < sSup s`, there is an element `a` in `s` with `b < a`, if `s` is nonempty and the order
is a linear order. -/
@[to_dual exists_lt_of_csInf_lt /-- When `sInf s < b`, there is an element `a` in `s` with `a < b`,
if `s` is nonempty and the order is a linear order. -/]
theorem exists_lt_of_lt_csSup (hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a := by
contrapose! hb
exact csSup_le hs hb

/-- When `sInf s < b`, there is an element `a` in `s` with `a < b`, if `s` is nonempty and the order
is a linear order. -/
theorem exists_lt_of_csInf_lt (hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b :=
exists_lt_of_lt_csSup (α := αᵒᵈ) hs hb

@[to_dual csInf_lt_iff]
theorem lt_csSup_iff (hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b :=
lt_isLUB_iff <| isLUB_csSup hs hb

theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b ∈ s, b < a :=
isGLB_lt_iff <| isGLB_csInf hs hb

@[simp] lemma csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
@[to_dual (attr := simp)]
lemma csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs

@[simp] lemma ciSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅ :=
@[to_dual (attr := simp)]
lemma ciSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅ :=
csSup_of_not_bddAbove hf

@[to_dual]
lemma csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ := by
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
contrapose hs
exact hs.mono (subset_univ _)

@[to_dual]
lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ :=
csSup_eq_univ_of_not_bddAbove hf

@[simp] lemma csInf_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf ∅ :=
ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow s hs

@[simp] lemma ciInf_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf ∅ :=
csInf_of_not_bddBelow hf

lemma csInf_eq_univ_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf univ :=
csSup_eq_univ_of_not_bddAbove (α := αᵒᵈ) hs

lemma ciInf_eq_univ_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf univ :=
csInf_eq_univ_of_not_bddBelow hf

/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
@[to_dual /-- When every element of a set `s` is bounded by an element of a set `t`, and conversely,
then `s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/]
theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
(hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
sSup s = sSup t := by
Expand Down Expand Up @@ -464,13 +430,6 @@ theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
exact hyx.trans (le_csSup Bs xs)
· simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]

/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/
theorem csInf_eq_csInf_of_forall_exists_le {s t : Set α}
(hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
sInf s = sInf t :=
csSup_eq_csSup_of_forall_exists_le (α := αᵒᵈ) hs ht

theorem csSup_union_le (s t : Set α) : sSup (s ∪ t) ≤ sSup s ⊔ sSup t := by
rcases s.eq_empty_or_nonempty with (rfl | hs)
· simp
Expand All @@ -489,12 +448,10 @@ lemma sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i,
lemma sInf_iUnion_Ici (f : ι → α) : sInf (⋃ (i : ι), Ici (f i)) = ⨅ i, f i :=
sSup_iUnion_Iic (α := αᵒᵈ) f

@[to_dual]
theorem csInf_eq_bot_of_bot_mem [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥ :=
eq_bot_iff.2 <| csInf_le (OrderBot.bddBelow s) hs

theorem csSup_eq_top_of_top_mem [OrderTop α] {s : Set α} (hs : ⊤ ∈ s) : sSup s = ⊤ :=
csInf_eq_bot_of_bot_mem (α := αᵒᵈ) hs

open Function

variable [WellFoundedLT α]
Expand Down Expand Up @@ -619,6 +576,8 @@ variable [ConditionallyCompleteLinearOrderBot α]

/-- The `sSup` of a non-empty set is its least upper bound for a conditionally
complete lattice with a top. -/
@[to_dual /-- The `sInf` of a non-empty set is its greatest lower bound for a conditionally
complete lattice with a bottom. -/]
theorem isLUB_sSup' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
(hs : s.Nonempty) : IsLUB s (sSup s) := by
classical
Expand Down Expand Up @@ -661,6 +620,8 @@ theorem isLUB_sSup (s : Set (WithTop α)) : IsLUB s (sSup s) := by

/-- The `sInf` of a bounded-below set is its greatest lower bound for a conditionally
complete lattice with a top. -/
@[to_dual /-- The `sSup` of a bounded-above set is its lowest upper bound for a conditionally
complete lattice with a bottom. -/]
theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
(hs : BddBelow s) : IsGLB s (sInf s) := by
classical
Expand Down
2 changes: 2 additions & 0 deletions Mathlib/Order/ConditionallyCompleteLattice/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,8 @@ class ConditionallyCompleteLinearOrder (α : Type*)
compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
compareOfLessAndEq_rfl

attribute [to_dual existing] ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove

/-- A conditionally complete linear order with `Bot` is a linear order with least element, in which
every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily
bounded below) has an infimum. A typical example is the natural numbers.
Expand Down
Loading
Loading