revert improvements

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -496,12 +496,13 @@ noncomputable def sequence_of_cubes : ℕ → { i : ι // valley cs ((cs i).shif
 | 0     := let v := valley_unit_cube h      in ⟨mi h v, valley_mi⟩
 | (k+1) := let v := (sequence_of_cubes k).2 in ⟨mi h v, valley_mi⟩
 
-def decreasing_sequence (k : ℕ) : ℝ := (cs (sequence_of_cubes h k).1).w
+def decreasing_sequence (k : ℕ) : order_dual ℝ :=
+(cs (sequence_of_cubes h k).1).w
 
-lemma strict_anti_sequence_of_cubes : strict_anti $ decreasing_sequence h :=
-strict_anti_nat_of_succ_lt $ λ k,
+lemma strict_mono_sequence_of_cubes : strict_mono $ decreasing_sequence h :=
+strict_mono_nat_of_lt_succ $
 begin
-  let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
+  intro k, let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
   apply w_lt_w h v (mi_mem_bcubes : mi h v ∈ _),
 end
 
@@ -511,7 +512,7 @@ theorem not_correct : ¬correct cs :=
 begin
   intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
-  intros n m hnm, apply (strict_anti_sequence_of_cubes h).injective,
+  intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
   dsimp only [decreasing_sequence], rw hnm
 end
 

src/algebra/tropical/basic.lean

@@ -24,7 +24,8 @@ well as the expected implementations of tropical addition and tropical multiplic
 
 ## Implementation notes
 
-The tropical structure relies on `has_top` and `min`. For the max-tropical numbers, use `Rᵒᵈ`.
+The tropical structure relies on `has_top` and `min`. For the max-tropical numbers, use
+`order_dual R`.
 
 Inspiration was drawn from the implementation of `additive`/`multiplicative`/`opposite`,
 where a type synonym is created with some barebones API, and quickly made irreducible.

src/analysis/convex/quasiconvex.lean

@@ -31,7 +31,7 @@ not hard but quite a pain to go about as there are many cases to consider.
 * https://en.wikipedia.org/wiki/Quasiconvex_function
 -/
 
-open function order_dual set
+open function set
 
 variables {𝕜 E F β : Type*}
 
@@ -62,9 +62,17 @@ quasiconvex_on 𝕜 s f ∧ quasiconcave_on 𝕜 s f
 
 variables {𝕜 s f}
 
-lemma quasiconvex_on.dual : quasiconvex_on 𝕜 s f → quasiconcave_on 𝕜 s (to_dual ∘ f) := id
-lemma quasiconcave_on.dual : quasiconcave_on 𝕜 s f → quasiconvex_on 𝕜 s (to_dual ∘ f) := id
-lemma quasilinear_on.dual : quasilinear_on 𝕜 s f → quasilinear_on 𝕜 s (to_dual ∘ f) := and.swap
+lemma quasiconvex_on.dual (hf : quasiconvex_on 𝕜 s f) :
+  @quasiconcave_on 𝕜 E (order_dual β) _ _ _ _ s f :=
+hf
+
+lemma quasiconcave_on.dual (hf : quasiconcave_on 𝕜 s f) :
+  @quasiconvex_on 𝕜 E (order_dual β) _ _ _ _ s f :=
+hf
+
+lemma quasilinear_on.dual (hf : quasilinear_on 𝕜 s f) :
+  @quasilinear_on 𝕜 E (order_dual β) _ _ _ _ s f :=
+⟨hf.2, hf.1⟩
 
 lemma convex.quasiconvex_on_of_convex_le (hs : convex 𝕜 s) (h : ∀ r, convex 𝕜 {x | f x ≤ r}) :
   quasiconvex_on 𝕜 s f :=

src/analysis/locally_convex/weak_dual.lean

@@ -101,8 +101,11 @@ begin
     let U' := hU₁.to_finset,
     by_cases hU₃ : U.fst.nonempty,
     { have hU₃' : U'.nonempty := (set.finite.to_finset.nonempty hU₁).mpr hU₃,
-      refine ⟨(U'.sup p).ball 0 $ U'.inf' hU₃' U.snd, p.basis_sets_mem _ $
-        (finset.lt_inf'_iff _ _).2 $ λ y hy, hU₂ y $ (hU₁.mem_to_finset).mp hy, λ x hx y hy, _⟩,
+      let r := U'.inf' hU₃' U.snd,
+      have hr : 0 < r :=
+      (finset.lt_inf'_iff hU₃' _).mpr (λ y hy, hU₂ y ((set.finite.mem_to_finset hU₁).mp hy)),
+      use [seminorm.ball (U'.sup p) (0 : E) r],
+      refine ⟨p.basis_sets_mem _ hr, λ x hx y hy, _⟩,
       simp only [set.mem_preimage, set.mem_pi, mem_ball_zero_iff],
       rw seminorm.mem_ball_zero at hx,
       rw ←linear_map.to_seminorm_family_apply,

src/data/finset/lattice.lean

@@ -327,13 +327,13 @@ lemma inf_mono (h : s₁ ⊆ s₂) : s₂.inf f ≤ s₁.inf f :=
 le_inf $ assume b hb, inf_le (h hb)
 
 @[simp] lemma lt_inf_iff [is_total α (≤)] {a : α} (ha : a < ⊤) : a < s.inf f ↔ (∀ b ∈ s, a < f b) :=
-@sup_lt_iff αᵒᵈ _ _ _ _ _ _ _ ha
+@sup_lt_iff (order_dual α) _ _ _ _ _ _ _ ha
 
 @[simp] lemma inf_le_iff [is_total α (≤)] {a : α} (ha : a < ⊤) : s.inf f ≤ a ↔ (∃ b ∈ s, f b ≤ a) :=
-@le_sup_iff αᵒᵈ _ _ _ _ _ _ _ ha
+@le_sup_iff (order_dual α) _ _ _ _ _ _ _ ha
 
 @[simp] lemma inf_lt_iff [is_total α (≤)] {a : α} : s.inf f < a ↔ (∃ b ∈ s, f b < a) :=
-@lt_sup_iff αᵒᵈ _ _ _ _ _ _ _
+@lt_sup_iff (order_dual α) _ _ _ _ _ _ _
 
 lemma inf_attach (s : finset β) (f : β → α) : s.attach.inf (λ x, f x) = s.inf f :=
 @sup_attach αᵒᵈ _ _ _ _ _
@@ -626,13 +626,13 @@ lemma inf'_le (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b := @le_sup' αᵒᵈ _
 @sup'_le_iff αᵒᵈ _ _ _ H f _
 
 @[simp] lemma lt_inf'_iff [is_total α (≤)] {a : α} : a < s.inf' H f ↔ (∀ b ∈ s, a < f b) :=
-@sup'_lt_iff αᵒᵈ _ _ _ H f _ _
+@sup'_lt_iff (order_dual α) _ _ _ H f _ _
 
 @[simp] lemma inf'_le_iff [is_total α (≤)] {a : α} : s.inf' H f ≤ a ↔ (∃ b ∈ s, f b ≤ a) :=
-@le_sup'_iff αᵒᵈ _ _ _ H f _ _
+@le_sup'_iff (order_dual α) _ _ _ H f _ _
 
 @[simp] lemma inf'_lt_iff [is_total α (≤)] {a : α} : s.inf' H f < a ↔ (∃ b ∈ s, f b < a) :=
-@lt_sup'_iff αᵒᵈ _ _ _ H f _ _
+@lt_sup'_iff (order_dual α) _ _ _ H f _ _
 
 lemma inf'_bUnion [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β}
   (Ht : ∀ b, (t b).nonempty) :
@@ -693,7 +693,7 @@ lemma inf_closed_of_inf_closed {s : set α} (t : finset α) (htne : t.nonempty)
 
 lemma exists_mem_eq_inf [is_total α (≤)] (s : finset β) (h : s.nonempty) (f : β → α) :
   ∃ a, a ∈ s ∧ s.inf f = f a :=
-@exists_mem_eq_sup αᵒᵈ _ _ _ _ _ h f
+@exists_mem_eq_sup (order_dual α) _ _ _ _ _ h f
 
 lemma coe_inf_of_nonempty {s : finset β} (h : s.nonempty) (f : β → α):
   (↑(s.inf f) : with_top α) = s.inf (λ i, f i) :=
@@ -904,15 +904,15 @@ lemma max'_eq_of_dual_min' {s : finset α} (hs : s.nonempty) :
   max' s hs = of_dual (min' (image to_dual s) (nonempty.image hs to_dual)) :=
 begin
   rw [of_dual, to_dual, equiv.coe_fn_mk, equiv.coe_fn_symm_mk, id.def],
-  simp_rw (@image_id αᵒᵈ (s : finset αᵒᵈ)),
+  simp_rw (@image_id (order_dual α) (s : finset (order_dual α))),
   refl,
 end
 
 lemma min'_eq_of_dual_max' {s : finset α} (hs : s.nonempty) :
   min' s hs = of_dual (max' (image to_dual s) (nonempty.image hs to_dual)) :=
 begin
   rw [of_dual, to_dual, equiv.coe_fn_mk, equiv.coe_fn_symm_mk, id.def],
-  simp_rw (@image_id αᵒᵈ (s : finset αᵒᵈ)),
+  simp_rw (@image_id (order_dual α) (s : finset (order_dual α))),
   refl,
 end
 

src/order/basic.lean

@@ -14,7 +14,7 @@ classes and allows to transfer order instances.
 
 ## Type synonyms
 
-* `order_dual α` : A type synonym reversing the meaning of all inequalities.
+* `order_dual α` : A type synonym reversing the meaning of all inequalities, with notation `αᵒᵈ`.
 * `as_linear_order α`: A type synonym to promote `partial_order α` to `linear_order α` using
   `is_total α (≤)`.
 
@@ -389,7 +389,8 @@ instance order.preimage.decidable {α β} (f : α → β) (s : β → β → Pro
 
 /-! ### Order dual -/
 
-/-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. -/
+/-- Type synonym to equip a type with the dual order: `≤` means `≥` and `<` means `>`. `αᵒᵈ` is
+notation for `order_dual α`. -/
 def order_dual (α : Type*) : Type* := α
 
 notation α `ᵒᵈ`:std.prec.max_plus := order_dual α

src/order/circular.lean

@@ -48,7 +48,7 @@ Some concrete circular orders one encounters in the wild are `zmod n` for `0 < n
 
 ## Notes
 
-There's an unsolved diamond here. The instances `has_le α → has_btw αᵒᵈ` and
+There's an unsolved diamond on `order_dual α` here. The instances `has_le α → has_btw αᵒᵈ` and
 `has_lt α → has_sbtw αᵒᵈ` can each be inferred in two ways:
 * `has_le α` → `has_btw α` → `has_btw αᵒᵈ` vs
   `has_le α` → `has_le αᵒᵈ` → `has_btw αᵒᵈ`

src/order/complete_lattice.lean

@@ -1162,9 +1162,6 @@ instance Prop.complete_lattice : complete_lattice Prop :=
   .. Prop.bounded_order,
   .. Prop.distrib_lattice }
 
-noncomputable instance Prop.complete_linear_order : complete_linear_order Prop :=
-{ ..Prop.complete_lattice, ..Prop.linear_order }
-
 @[simp] lemma Sup_Prop_eq {s : set Prop} : Sup s = ∃ p ∈ s, p := rfl
 @[simp] lemma Inf_Prop_eq {s : set Prop} : Inf s = ∀ p ∈ s, p := rfl
 

src/order/galois_connection.lean

@@ -41,8 +41,7 @@ This means the infimum of subgroups will be defined to be the intersection of se
 with a proof that intersection of subgroups is a subgroup, rather than the closure of the
 intersection.
 -/
-
-open function order_dual set
+open function order set
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {κ : ι → Sort*} {a a₁ a₂ : α}
@@ -544,22 +543,22 @@ structure galois_coinsertion {α β : Type*} [preorder α] [preorder β] (l : α
 
 /-- Make a `galois_insertion u l` in the `order_dual`, from a `galois_coinsertion l u` -/
 def galois_coinsertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_coinsertion l u → galois_insertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) :=
+  galois_coinsertion l u → @galois_insertion (order_dual β) (order_dual α) _ _ u l :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_coinsertion u l` in the `order_dual`, from a `galois_insertion l u` -/
 def galois_insertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_insertion l u → galois_coinsertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) :=
+  galois_insertion l u → @galois_coinsertion (order_dual β) (order_dual α) _ _ u l :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_coinsertion l u` from a `galois_insertion l u` in the `order_dual` -/
 def galois_coinsertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_insertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) → galois_coinsertion l u :=
+  @galois_insertion (order_dual β) (order_dual α) _ _ u l → galois_coinsertion l u :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_insertion l u` from a `galois_coinsertion l u` in the `order_dual` -/
 def galois_insertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_coinsertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) → galois_insertion l u :=
+  @galois_coinsertion (order_dual β) (order_dual α) _ _ u l → galois_insertion l u :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Makes a Galois coinsertion from an order-preserving bijection. -/

src/order/ord_continuous.lean

@@ -23,7 +23,7 @@ universes u v w x
 
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
 
-open function order_dual set
+open set function
 
 /-!
 ### Definitions
@@ -51,8 +51,8 @@ protected lemma id : left_ord_continuous (id : α → α) := λ s x h, by simpa
 
 variable {α}
 
-protected lemma order_dual : left_ord_continuous f → right_ord_continuous (to_dual ∘ f ∘ of_dual) :=
-id
+protected lemma order_dual (hf : left_ord_continuous f) :
+  @right_ord_continuous (order_dual α) (order_dual β) _ _ f := hf
 
 lemma map_is_greatest (hf : left_ord_continuous f) {s : set α} {x : α} (h : is_greatest s x):
   is_greatest (f '' s) (f x) :=
@@ -148,8 +148,8 @@ protected lemma id : right_ord_continuous (id : α → α) := λ s x h, by simpa
 
 variable {α}
 
-protected lemma order_dual : right_ord_continuous f → left_ord_continuous (to_dual ∘ f ∘ of_dual) :=
-id
+protected lemma order_dual (hf : right_ord_continuous f) :
+  @left_ord_continuous (order_dual α) (order_dual β) _ _ f := hf
 
 lemma map_is_least (hf : right_ord_continuous f) {s : set α} {x : α} (h : is_least s x):
   is_least (f '' s) (f x) :=