Skip to content

chore(Order/UpperLower/Basic): use to_dual #34640

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
vihdzp wants to merge 4 commits into
base: master
Choose a base branch
from
+27 −78
Open

chore(Order/UpperLower/Basic): use to_dual #34640

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7d52e54
finish
vihdzp Jan 31, 2026
4fbffb7
Update Basic.lean
vihdzp Jan 31, 2026
01d7fe1
Update Basic.lean
vihdzp Jan 31, 2026
a1305bb
Merge branch 'master' into dualize
vihdzp Feb 11, 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
20 changes: 4 additions & 16 deletions Mathlib/Order/Interval/Set/LinearOrder.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,34 +24,22 @@ namespace Set

variable {α : Type*} [LinearOrder α] {a a₁ a₂ b b₁ b₂ c d : α}

@[to_dual]
theorem notMem_Ici : c ∉ Ici a ↔ c < a :=
not_le

theorem notMem_Iic : c ∉ Iic b ↔ b < c :=
not_le

@[to_dual]
theorem notMem_Ioi : c ∉ Ioi a ↔ c ≤ a :=
not_lt

theorem notMem_Iio : c ∉ Iio b ↔ b ≤ c :=
not_lt

@[simp]
@[to_dual (attr := simp)]
theorem compl_Iic : (Iic a)ᶜ = Ioi a :=
Copy link
Contributor

@JovanGerb JovanGerb Feb 11, 2026

Choose a reason for hiding this comment

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

I have this other PR #33543 where I teach to_dual that compl should be translated to hnot. I guess that that is a bad idea...

Copy link
Collaborator Author

@vihdzp vihdzp Feb 11, 2026

Choose a reason for hiding this comment

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

We already avoid translating the order on sets, don't we? So I don't think this should cause any conflict.

Copy link
Contributor

@JovanGerb JovanGerb Feb 11, 2026

Choose a reason for hiding this comment

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

Yes, but I mean that the name translation will get messed up.

Copy link
Collaborator

@Komyyy Komyyy Feb 11, 2026

Choose a reason for hiding this comment

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

Ideally, compl should be translated to hnot only when the type is not a boolean algebra.
However, we need to implement a new feature for the to_dual attribute to do this...

Copy link
Collaborator

@Komyyy Komyyy Feb 11, 2026

Choose a reason for hiding this comment

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

Rather than doing that, I think it would be better to stop using compl in the definition of Heyting algebras and make compl a notation exclusively for Boolean algebras.

ext fun _ => not_le

@[simp]
theorem compl_Ici : (Ici a)ᶜ = Iio a :=
ext fun _ => not_le

@[simp]
@[to_dual (attr := simp)]
theorem compl_Iio : (Iio a)ᶜ = Ici a :=
ext fun _ => not_lt

@[simp]
theorem compl_Ioi : (Ioi a)ᶜ = Iic a :=
ext fun _ => not_lt

@[simp]
theorem Ici_diff_Ici : Ici a \ Ici b = Ico a b := by rw [diff_eq, compl_Ici, Ici_inter_Iio]

Expand Down
6 changes: 2 additions & 4 deletions Mathlib/Order/Interval/Set/OrderEmbedding.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,8 @@ section Preorder

variable [Preorder α] [Preorder β] (e : α ↪o β) (x y : α)

@[simp] theorem preimage_Ici : e ⁻¹' Ici (e x) = Ici x := ext fun _ ↦ e.le_iff_le
@[simp] theorem preimage_Iic : e ⁻¹' Iic (e x) = Iic x := ext fun _ ↦ e.le_iff_le
@[simp] theorem preimage_Ioi : e ⁻¹' Ioi (e x) = Ioi x := ext fun _ ↦ e.lt_iff_lt
@[simp] theorem preimage_Iio : e ⁻¹' Iio (e x) = Iio x := ext fun _ ↦ e.lt_iff_lt
@[to_dual (attr := simp)] theorem preimage_Ici : e ⁻¹' Ici (e x) = Ici x := ext fun _ ↦ e.le_iff_le
@[to_dual (attr := simp)] theorem preimage_Ioi : e ⁻¹' Ioi (e x) = Ioi x := ext fun _ ↦ e.lt_iff_lt

@[simp] theorem preimage_Icc : e ⁻¹' Icc (e x) (e y) = Icc x y := by ext; simp
@[simp] theorem preimage_Ico : e ⁻¹' Ico (e x) (e y) = Ico x y := by ext; simp
Expand Down
77 changes: 19 additions & 58 deletions Mathlib/Order/UpperLower/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,39 +118,30 @@ section Preorder

variable [Preorder α] [Preorder β] {s : Set α} {p : α → Prop} (a : α)

theorem isUpperSet_Ici : IsUpperSet (Ici a) := fun _ _ => ge_trans

theorem isLowerSet_Iic : IsLowerSet (Iic a) := fun _ _ => le_trans

theorem isUpperSet_Ioi : IsUpperSet (Ioi a) := fun _ _ => flip lt_of_lt_of_le

theorem isLowerSet_Iio : IsLowerSet (Iio a) := fun _ _ => lt_of_le_of_lt
@[to_dual] theorem isUpperSet_Ici : IsUpperSet (Ici a) := fun _ _ => ge_trans
@[to_dual] theorem isUpperSet_Ioi : IsUpperSet (Ioi a) := fun _ _ => flip lt_of_lt_of_le

@[to_dual]
theorem isUpperSet_iff_Ici_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ici a ⊆ s := by
simp [IsUpperSet, subset_def, @forall_swap (_ ∈ s)]

theorem isLowerSet_iff_Iic_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iic a ⊆ s := by
simp [IsLowerSet, subset_def, @forall_swap (_ ∈ s)]

alias ⟨IsUpperSet.Ici_subset, _⟩ := isUpperSet_iff_Ici_subset

alias ⟨IsLowerSet.Iic_subset, _⟩ := isLowerSet_iff_Iic_subset
@[to_dual] alias ⟨IsUpperSet.Ici_subset, _⟩ := isUpperSet_iff_Ici_subset

@[to_dual]
theorem IsUpperSet.Ioi_subset (h : IsUpperSet s) ⦃a⦄ (ha : a ∈ s) : Ioi a ⊆ s :=
Ioi_subset_Ici_self.trans <| h.Ici_subset ha

theorem IsLowerSet.Iio_subset (h : IsLowerSet s) ⦃a⦄ (ha : a ∈ s) : Iio a ⊆ s :=
h.toDual.Ioi_subset ha

theorem IsUpperSet.ordConnected (h : IsUpperSet s) : s.OrdConnected :=
⟨fun _ ha _ _ => Icc_subset_Ici_self.trans <| h.Ici_subset ha⟩

@[to_dual existing]
Copy link
Contributor

@JovanGerb JovanGerb Feb 12, 2026

Choose a reason for hiding this comment

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

Can you add a comment here saying that to_dual cannot yet reorder arguments of arguments? That way it'll be easier to clean up later

theorem IsLowerSet.ordConnected (h : IsLowerSet s) : s.OrdConnected :=
⟨fun _ _ _ hb => Icc_subset_Iic_self.trans <| h.Iic_subset hb⟩

theorem IsUpperSet.preimage (hs : IsUpperSet s) {f : β → α} (hf : Monotone f) :
IsUpperSet (f ⁻¹' s : Set β) := fun _ _ h => hs <| hf h

@[to_dual existing]
theorem IsLowerSet.preimage (hs : IsLowerSet s) {f : β → α} (hf : Monotone f) :
IsLowerSet (f ⁻¹' s : Set β) := fun _ _ h => hs <| hf h

Expand All @@ -160,24 +151,18 @@ theorem IsUpperSet.image (hs : IsUpperSet s) (f : α ≃o β) : IsUpperSet (f ''
rw [Equiv.image_eq_preimage_symm]
exact hs.preimage f.symm.monotone

@[to_dual]
theorem OrderEmbedding.image_Ici (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
e '' Ici a = Ici (e a) := by
rw [← e.preimage_Ici, image_preimage_eq_inter_range,
inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

theorem OrderEmbedding.image_Iic (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
e '' Iic a = Iic (e a) :=
e.dual.image_Ici he a

@[to_dual]
theorem OrderEmbedding.image_Ioi (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
e '' Ioi a = Ioi (e a) := by
rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]

theorem OrderEmbedding.image_Iio (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
e '' Iio a = Iio (e a) :=
e.dual.image_Ioi he a

@[simp]
theorem Set.monotone_mem : Monotone (· ∈ s) ↔ IsUpperSet s :=
Iff.rfl
Expand All @@ -194,12 +179,10 @@ theorem isUpperSet_setOf : IsUpperSet { a | p a } ↔ Monotone p :=
theorem isLowerSet_setOf : IsLowerSet { a | p a } ↔ Antitone p :=
forall_swap

@[to_dual]
lemma IsUpperSet.upperBounds_subset (hs : IsUpperSet s) : s.Nonempty → upperBounds s ⊆ s :=
fun ⟨_a, ha⟩ _b hb ↦ hs (hb ha) ha

lemma IsLowerSet.lowerBounds_subset (hs : IsLowerSet s) : s.Nonempty → lowerBounds s ⊆ s :=
fun ⟨_a, ha⟩ _b hb ↦ hs (hb ha) ha

section OrderTop

variable [OrderTop α]
Expand All @@ -222,36 +205,22 @@ section NoMaxOrder

variable [NoMaxOrder α]

@[to_dual]
theorem IsUpperSet.not_bddAbove (hs : IsUpperSet s) : s.Nonempty → ¬BddAbove s := by
rintro ⟨a, ha⟩ ⟨b, hb⟩
obtain ⟨c, hc⟩ := exists_gt b
exact hc.not_ge (hb <| hs ((hb ha).trans hc.le) ha)

@[to_dual]
theorem not_bddAbove_Ici : ¬BddAbove (Ici a) :=
(isUpperSet_Ici _).not_bddAbove nonempty_Ici

@[to_dual]
theorem not_bddAbove_Ioi : ¬BddAbove (Ioi a) :=
(isUpperSet_Ioi _).not_bddAbove nonempty_Ioi

end NoMaxOrder

section NoMinOrder

variable [NoMinOrder α]

theorem IsLowerSet.not_bddBelow (hs : IsLowerSet s) : s.Nonempty → ¬BddBelow s := by
rintro ⟨a, ha⟩ ⟨b, hb⟩
obtain ⟨c, hc⟩ := exists_lt b
exact hc.not_ge (hb <| hs (hc.le.trans <| hb ha) ha)

theorem not_bddBelow_Iic : ¬BddBelow (Iic a) :=
(isLowerSet_Iic _).not_bddBelow nonempty_Iic

theorem not_bddBelow_Iio : ¬BddBelow (Iio a) :=
(isLowerSet_Iio _).not_bddBelow nonempty_Iio

end NoMinOrder

end Preorder

section PartialOrder
Expand All @@ -262,12 +231,10 @@ variable [PartialOrder α] {s : Set α}
theorem isUpperSet_iff_forall_lt : IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s :=
forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

@[to_dual]
theorem isUpperSet_iff_Ioi_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ioi a ⊆ s := by
simp [isUpperSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

theorem isLowerSet_iff_Iio_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s := by
simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

end PartialOrder

section LinearOrder
Expand All @@ -283,23 +250,17 @@ theorem IsUpperSet.total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t
· exact hbs (hs hab has)
· exact hat (ht hba hbt)

@[to_dual]
theorem IsUpperSet.eq_empty_or_Ici [WellFoundedLT α] (h : IsUpperSet s) :
s = ∅ ∨ (∃ a, s = Set.Ici a) := by
s = ∅ ∨ ∃ a, s = Ici a := by
refine or_iff_not_imp_left.2 fun ha ↦ ?_
obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha
exact ⟨_, Set.ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩

theorem IsLowerSet.eq_empty_or_Iic [WellFoundedGT α] (h : IsLowerSet s) :
s = ∅ ∨ (∃ a, s = Set.Iic a) :=
IsUpperSet.eq_empty_or_Ici (α := αᵒᵈ) h
exact ⟨_, ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩

@[to_dual]
theorem IsLowerSet.eq_univ_or_Iio [WellFoundedLT α] (h : IsLowerSet s) :
s = .univ ∨ (∃ a, s = Set.Iio a) := by
s = univ ∨ ∃ a, s = Iio a := by
simp_rw [← @compl_inj_iff _ s]
simpa using h.compl.eq_empty_or_Ici

theorem IsUpperSet.eq_univ_or_Ioi [WellFoundedGT α] (h : IsUpperSet s) :
s = .univ ∨ (∃ a, s = Set.Ioi a) :=
IsLowerSet.eq_univ_or_Iio (α := αᵒᵈ) h

end LinearOrder
2 changes: 2 additions & 0 deletions Mathlib/Order/WellFounded.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,8 @@ section LinearOrder

variable [LinearOrder β] [Preorder γ]

-- TODO: the name `WellFounded.min` is incorrect when the assumption is that `>` is well-founded.
@[to_dual none]
theorem WellFounded.min_le (h : WellFounded ((· < ·) : β → β → Prop))
Comment on lines +142 to 143
Copy link
Contributor

@JovanGerb JovanGerb Feb 12, 2026

Choose a reason for hiding this comment

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

Why is this in this PR? And shouldn't we just change it to h : WellFoundedLT β?

{x : β} {s : Set β} (hx : x ∈ s) (hne : s.Nonempty := ⟨x, hx⟩) : h.min s hne ≤ x :=
not_lt.1 <| h.not_lt_min _ _ hx
Expand Down
Loading