feat(order/upper_lower/basic): Linear order (#19068)

Upper/lower sets on a linear order themselves form a linear order.

Author: YaelDillies

src/algebra/order/upper_lower.lean

@@ -34,13 +34,10 @@ section ordered_comm_group
 variables {α : Type*} [ordered_comm_group α] {s t : set α} {a : α}
 
 @[to_additive] lemma is_upper_set.smul (hs : is_upper_set s) : is_upper_set (a • s) :=
-begin
-  rintro _ y hxy ⟨x, hx, rfl⟩,
-  exact mem_smul_set_iff_inv_smul_mem.2 (hs (le_inv_mul_iff_mul_le.2 hxy) hx),
-end
+hs.image $ order_iso.mul_left _
 
 @[to_additive] lemma is_lower_set.smul (hs : is_lower_set s) : is_lower_set (a • s) :=
-hs.of_dual.smul
+hs.image $ order_iso.mul_left _
 
 @[to_additive] lemma set.ord_connected.smul (hs : s.ord_connected) : (a • s).ord_connected :=
 begin
@@ -55,10 +52,10 @@ by { rw [←smul_eq_mul, ←bUnion_smul_set], exact is_upper_set_Union₂ (λ x
 by { rw mul_comm, exact hs.mul_left }
 
 @[to_additive] lemma is_lower_set.mul_left (ht : is_lower_set t) : is_lower_set (s * t) :=
-ht.of_dual.mul_left
+ht.to_dual.mul_left
 
 @[to_additive] lemma is_lower_set.mul_right (hs : is_lower_set s) : is_lower_set (s * t) :=
-hs.of_dual.mul_right
+hs.to_dual.mul_right
 
 @[to_additive] lemma is_upper_set.inv (hs : is_upper_set s) : is_lower_set s⁻¹ :=
 λ x y h, hs $ inv_le_inv' h
@@ -73,10 +70,10 @@ by { rw div_eq_mul_inv, exact ht.inv.mul_left }
 by { rw div_eq_mul_inv, exact hs.mul_right }
 
 @[to_additive] lemma is_lower_set.div_left (ht : is_lower_set t) : is_upper_set (s / t) :=
-ht.of_dual.div_left
+ht.to_dual.div_left
 
 @[to_additive] lemma is_lower_set.div_right (hs : is_lower_set s) : is_lower_set (s / t) :=
-hs.of_dual.div_right
+hs.to_dual.div_right
 
 namespace upper_set
 

src/order/upper_lower/basic.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies, Sara Rousta
 import data.set_like.basic
 import data.set.intervals.ord_connected
 import data.set.intervals.order_iso
+import tactic.by_contra
 
 /-!
 # Up-sets and down-sets
@@ -135,10 +136,10 @@ iff.rfl
 @[simp] lemma is_upper_set_preimage_to_dual_iff {s : set αᵒᵈ} :
   is_upper_set (to_dual ⁻¹' s) ↔ is_lower_set s := iff.rfl
 
-alias is_lower_set_preimage_of_dual_iff ↔ _ is_upper_set.of_dual
-alias is_upper_set_preimage_of_dual_iff ↔ _ is_lower_set.of_dual
-alias is_lower_set_preimage_to_dual_iff ↔ _ is_upper_set.to_dual
-alias is_upper_set_preimage_to_dual_iff ↔ _ is_lower_set.to_dual
+alias is_lower_set_preimage_of_dual_iff ↔ _ is_upper_set.to_dual
+alias is_upper_set_preimage_of_dual_iff ↔ _ is_lower_set.to_dual
+alias is_lower_set_preimage_to_dual_iff ↔ _ is_upper_set.of_dual
+alias is_upper_set_preimage_to_dual_iff ↔ _ is_lower_set.of_dual
 
 end has_le
 
@@ -266,6 +267,24 @@ alias is_lower_set_iff_Iio_subset ↔ is_lower_set.Iio_subset _
 
 end partial_order
 
+section linear_order
+variables [linear_order α] {s t : set α}
+
+lemma is_upper_set.total (hs : is_upper_set s) (ht : is_upper_set t) : s ⊆ t ∨ t ⊆ s :=
+begin
+  by_contra' h,
+  simp_rw set.not_subset at h,
+  obtain ⟨⟨a, has, hat⟩, b, hbt, hbs⟩ := h,
+  obtain hab | hba := le_total a b,
+  { exact hbs (hs hab has) },
+  { exact hat (ht hba hbt) }
+end
+
+lemma is_lower_set.total (hs : is_lower_set s) (ht : is_lower_set t) : s ⊆ t ∨ t ⊆ s :=
+hs.to_dual.total ht.to_dual
+
+end linear_order
+
 /-! ### Bundled upper/lower sets -/
 
 section has_le
@@ -519,6 +538,32 @@ end lower_set
 
 end has_le
 
+section linear_order
+variables [linear_order α]
+
+instance upper_set.is_total_le : is_total (upper_set α) (≤) := ⟨λ s t, t.upper.total s.upper⟩
+instance lower_set.is_total_le : is_total (lower_set α) (≤) := ⟨λ s t, s.lower.total t.lower⟩
+
+noncomputable instance : complete_linear_order (upper_set α) :=
+{ le_total := is_total.total,
+  decidable_le := classical.dec_rel _,
+  decidable_eq := classical.dec_rel _,
+  decidable_lt := classical.dec_rel _,
+  max_def := by classical; exact sup_eq_max_default,
+  min_def := by classical; exact inf_eq_min_default,
+  ..upper_set.complete_distrib_lattice }
+
+noncomputable instance : complete_linear_order (lower_set α) :=
+{ le_total := is_total.total,
+  decidable_le := classical.dec_rel _,
+  decidable_eq := classical.dec_rel _,
+  decidable_lt := classical.dec_rel _,
+  max_def := by classical; exact sup_eq_max_default,
+  min_def := by classical; exact inf_eq_min_default,
+  ..lower_set.complete_distrib_lattice }
+
+end linear_order
+
 /-! #### Map -/
 
 section

src/topology/algebra/order/upper_lower.lean

@@ -85,7 +85,7 @@ protected lemma is_upper_set.interior (h : is_upper_set s) : is_upper_set (inter
 by { rw [←is_lower_set_compl, ←closure_compl], exact h.compl.closure }
 
 protected lemma is_lower_set.interior (h : is_lower_set s) : is_lower_set (interior s) :=
-h.of_dual.interior
+h.to_dual.interior
 
 protected lemma set.ord_connected.interior (h : s.ord_connected) : (interior s).ord_connected :=
 begin