[Merged by Bors] - feat(order/basic): Notation for order_dual

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

@@ -496,13 +496,12 @@ 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 : ℕ) : order_dual ℝ :=
-(cs (sequence_of_cubes h k).1).w
+def decreasing_sequence (k : ℕ) : ℝ := (cs (sequence_of_cubes h k).1).w
 
-lemma strict_mono_sequence_of_cubes : strict_mono $ decreasing_sequence h :=
-strict_mono_nat_of_lt_succ $
+lemma strict_anti_sequence_of_cubes : strict_anti $ decreasing_sequence h :=
+strict_anti_nat_of_succ_lt $ λ k,
 begin
-  intro k, let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
+  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
 
@@ -512,7 +511,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_mono.injective (strict_mono_sequence_of_cubes h),
+  intros n m hnm, apply (strict_anti_sequence_of_cubes h).injective,
   dsimp only [decreasing_sequence], rw hnm
 end
 

src/algebra/big_operators/multiset.lean

@@ -314,7 +314,7 @@ prod_le_prod_of_rel_le $ rel_map_left.2 $ rel_refl_of_refl_on h
 
 @[to_additive]
 lemma prod_le_sum_prod (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.prod ≤ (s.map f).prod :=
-@prod_map_le_prod (order_dual α) _ _ f h
+@prod_map_le_prod αᵒᵈ _ _ f h
 
 @[to_additive card_nsmul_le_sum]
 lemma pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ s.card ≤ s.prod :=

src/algebra/big_operators/order.lean

@@ -161,7 +161,7 @@ end
 
 @[to_additive sum_eq_zero_iff_of_nonneg]
 lemma prod_eq_one_iff_of_le_one' : (∀ i ∈ s, f i ≤ 1) → (∏ i in s, f i = 1 ↔ ∀ i ∈ s, f i = 1) :=
-@prod_eq_one_iff_of_one_le' _ (order_dual N) _ _ _
+@prod_eq_one_iff_of_one_le' _ Nᵒᵈ _ _ _
 
 @[to_additive single_le_sum]
 lemma single_le_prod' (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) : f a ≤ (∏ x in s, f x) :=
@@ -181,7 +181,7 @@ end
 @[to_additive card_nsmul_le_sum]
 lemma pow_card_le_prod (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
   n ^ s.card ≤ s.prod f :=
-@finset.prod_le_pow_card _ (order_dual N) _ _ _ _ h
+@finset.prod_le_pow_card _ Nᵒᵈ _ _ _ _ h
 
 lemma card_bUnion_le_card_mul [decidable_eq β] (s : finset ι) (f : ι → finset β) (n : ℕ)
   (h : ∀ a ∈ s, (f a).card ≤ n) :
@@ -204,7 +204,7 @@ calc (∏ y in t, ∏ x in s.filter (λ x, g x = y), f x) ≤
 lemma prod_le_prod_fiberwise_of_prod_fiber_le_one' {t : finset ι'}
   {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, (∏ x in s.filter (λ x, g x = y), f x) ≤ 1) :
   (∏ x in s, f x) ≤ ∏ y in t, ∏ x in s.filter (λ x, g x = y), f x :=
-@prod_fiberwise_le_prod_of_one_le_prod_fiber' _ (order_dual N) _ _ _ _ _ _ _ h
+@prod_fiberwise_le_prod_of_one_le_prod_fiber' _ Nᵒᵈ _ _ _ _ _ _ _ h
 
 end ordered_comm_monoid
 

src/algebra/bounds.lean

@@ -69,11 +69,11 @@ image2_subset_iff.2 $ λ x hx y hy, mul_mem_upper_bounds_mul hx hy
 
 @[to_additive] lemma mul_mem_lower_bounds_mul {s t : set M} {a b : M} (ha : a ∈ lower_bounds s)
   (hb : b ∈ lower_bounds t) : a * b ∈ lower_bounds (s * t) :=
-@mul_mem_upper_bounds_mul (order_dual M) _ _ _ _ _ _ _ _ ha hb
+@mul_mem_upper_bounds_mul Mᵒᵈ _ _ _ _ _ _ _ _ ha hb
 
 @[to_additive] lemma subset_lower_bounds_mul (s t : set M) :
   lower_bounds s * lower_bounds t ⊆ lower_bounds (s * t) :=
-@subset_upper_bounds_mul (order_dual M) _ _ _ _ _ _
+@subset_upper_bounds_mul Mᵒᵈ _ _ _ _ _ _
 
 @[to_additive] lemma bdd_above.mul {s t : set M} (hs : bdd_above s) (ht : bdd_above t) :
   bdd_above (s * t) :=

src/algebra/group_power/order.lean

@@ -34,8 +34,7 @@ theorem one_le_pow_of_one_le' {a : M} (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
 | (k + 1) := by { rw pow_succ, exact one_le_mul H (one_le_pow_of_one_le' k) }
 
 @[to_additive nsmul_nonpos]
-theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 :=
-@one_le_pow_of_one_le' (order_dual M) _ _ _ _ H n
+lemma pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 := @one_le_pow_of_one_le' Mᵒᵈ _ _ _ _ H n
 
 @[to_additive nsmul_le_nsmul]
 theorem pow_le_pow' {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
@@ -45,7 +44,7 @@ calc a ^ n ≤ a ^ n * a ^ k : le_mul_of_one_le_right' (one_le_pow_of_one_le' ha
 
 @[to_additive nsmul_le_nsmul_of_nonpos]
 theorem pow_le_pow_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
-@pow_le_pow' (order_dual M) _ _ _ _ _ _  ha h
+@pow_le_pow' Mᵒᵈ _ _ _ _ _ _  ha h
 
 @[to_additive nsmul_pos]
 theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k :=
@@ -59,8 +58,8 @@ begin
 end
 
 @[to_additive nsmul_neg]
-theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
-@one_lt_pow' (order_dual M) _ _ _ _ ha k hk
+lemma pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
+@one_lt_pow' Mᵒᵈ _ _ _ _ ha k hk
 
 @[to_additive nsmul_lt_nsmul]
 theorem pow_lt_pow' [covariant_class M M (*) (<)] {a : M} {n m : ℕ} (ha : 1 < a) (h : n < m) :
@@ -88,7 +87,7 @@ lemma one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x
 
 @[to_additive]
 lemma pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
-@one_le_pow_iff (order_dual M) _ _ _ _ _ hn
+@one_le_pow_iff Mᵒᵈ _ _ _ _ _ hn
 
 @[to_additive nsmul_pos_iff]
 lemma one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=

src/algebra/indicator_function.lean

@@ -447,7 +447,7 @@ if ha : a ∈ s then by simpa [ha] using hfg ha else by simpa [ha] using hg ha
 
 @[to_additive] lemma le_mul_indicator_apply {y} (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 1) :
   y ≤ mul_indicator s g a :=
-@mul_indicator_apply_le' α (order_dual M) ‹_› _ _ _ _ _ hfg hf
+@mul_indicator_apply_le' α Mᵒᵈ ‹_› _ _ _ _ _ hfg hf
 
 @[to_additive] lemma le_mul_indicator (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 1) :
   f ≤ mul_indicator s g :=
@@ -537,7 +537,7 @@ end
 
 lemma indicator_nonpos_le_indicator {β} [linear_order β] [has_zero β] (s : set α) (f : α → β) :
   {x | f x ≤ 0}.indicator f ≤ s.indicator f :=
-@indicator_le_indicator_nonneg α (order_dual β) _ _ s f
+@indicator_le_indicator_nonneg α βᵒᵈ _ _ s f
 
 end set
 

src/algebra/order/archimedean.lean

@@ -37,8 +37,7 @@ such that `0 < y` there exists a natural number `n` such that `x ≤ n • y`. -
 class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
 (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)
 
-instance order_dual.archimedean [ordered_add_comm_group α] [archimedean α] :
-  archimedean (order_dual α) :=
+instance order_dual.archimedean [ordered_add_comm_group α] [archimedean α] : archimedean αᵒᵈ :=
 ⟨λ x y hy, let ⟨n, hn⟩ := archimedean.arch (-x : α) (neg_pos.2 hy) in
   ⟨n, by rwa [neg_nsmul, neg_le_neg_iff] at hn⟩⟩
 

src/algebra/order/field.lean

@@ -706,11 +706,11 @@ eq.symm $ monotone.map_max (λ x y, div_le_div_of_le hc)
 
 lemma min_div_div_right_of_nonpos {c : α} (hc : c ≤ 0) (a b : α) :
   min (a / c) (b / c) = (max a b) / c :=
-eq.symm $ @monotone.map_max α (order_dual α) _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
+eq.symm $ @monotone.map_max α αᵒᵈ _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
 
 lemma max_div_div_right_of_nonpos {c : α} (hc : c ≤ 0) (a b : α) :
   max (a / c) (b / c) = (min a b) / c :=
-eq.symm $ @monotone.map_min α (order_dual α) _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
+eq.symm $ @monotone.map_min α αᵒᵈ _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
 
 lemma abs_div (a b : α) : |a / b| = |a| / |b| := (abs_hom : α →*₀ α).map_div a b
 

src/algebra/order/group.lean

@@ -91,14 +91,14 @@ instance ordered_comm_group.has_exists_mul_of_le (α : Type u)
   has_exists_mul_of_le α :=
 ⟨λ a b hab, ⟨b * a⁻¹, (mul_inv_cancel_comm_assoc a b).symm⟩⟩
 
-@[to_additive] instance [h : has_inv α] : has_inv (order_dual α) := h
-@[to_additive] instance [h : has_div α] : has_div (order_dual α) := h
-@[to_additive] instance [h : has_involutive_inv α] : has_involutive_inv (order_dual α) := h
-@[to_additive] instance [h : div_inv_monoid α] : div_inv_monoid (order_dual α) := h
-@[to_additive] instance [h : group α] : group (order_dual α) := h
-@[to_additive] instance [h : comm_group α] : comm_group (order_dual α) := h
-
-@[to_additive] instance [ordered_comm_group α] : ordered_comm_group (order_dual α) :=
+@[to_additive] instance [h : has_inv α] : has_inv αᵒᵈ := h
+@[to_additive] instance [h : has_div α] : has_div αᵒᵈ := h
+@[to_additive] instance [h : has_involutive_inv α] : has_involutive_inv αᵒᵈ := h
+@[to_additive] instance [h : div_inv_monoid α] : div_inv_monoid αᵒᵈ := h
+@[to_additive] instance [h : group α] : group αᵒᵈ := h
+@[to_additive] instance [h : comm_group α] : comm_group αᵒᵈ := h
+
+@[to_additive] instance [ordered_comm_group α] : ordered_comm_group αᵒᵈ :=
 { .. order_dual.ordered_comm_monoid, .. order_dual.group }
 
 section group
@@ -292,7 +292,7 @@ variable (α)
 
 /-- `x ↦ x⁻¹` as an order-reversing equivalence. -/
 @[to_additive "`x ↦ -x` as an order-reversing equivalence.", simps]
-def order_iso.inv : α ≃o order_dual α :=
+def order_iso.inv : α ≃o αᵒᵈ :=
 { to_equiv := (equiv.inv α).trans order_dual.to_dual,
   map_rel_iff' := λ a b, @inv_le_inv_iff α _ _ _ _ _ _ }
 
@@ -853,7 +853,7 @@ calc a ≤ b * (b⁻¹ * c) : h _ (lt_inv_mul_iff_lt.mpr hc)
 
 @[to_additive]
 lemma le_of_forall_lt_one_mul_le (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b :=
-@le_of_forall_one_lt_le_mul (order_dual α) _ _ _ _ _ _ h
+@le_of_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _ h
 
 @[to_additive]
 lemma le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=
@@ -866,7 +866,7 @@ lemma le_iff_forall_one_lt_le_mul : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε
 
 @[to_additive]
 lemma le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
-@le_iff_forall_one_lt_le_mul (order_dual α) _ _ _ _ _ _
+@le_iff_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _
 
 end densely_ordered
 
@@ -897,7 +897,7 @@ multiplication is monotone. -/
 class linear_ordered_comm_group (α : Type u) extends ordered_comm_group α, linear_order α
 
 @[to_additive] instance [linear_ordered_comm_group α] :
-  linear_ordered_comm_group (order_dual α) :=
+  linear_ordered_comm_group αᵒᵈ :=
 { .. order_dual.ordered_comm_group, .. order_dual.linear_order α }
 
 section linear_ordered_comm_group
@@ -933,11 +933,11 @@ mul_lt_mul_left' h c
 
 @[to_additive min_neg_neg]
 lemma min_inv_inv' (a b : α) : min (a⁻¹) (b⁻¹) = (max a b)⁻¹ :=
-eq.symm $ @monotone.map_max α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
+eq.symm $ @monotone.map_max α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
 
 @[to_additive max_neg_neg]
 lemma max_inv_inv' (a b : α) : max (a⁻¹) (b⁻¹) = (min a b)⁻¹ :=
-eq.symm $ @monotone.map_min α (order_dual α) _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
+eq.symm $ @monotone.map_min α αᵒᵈ _ _ has_inv.inv a b $ λ a b, inv_le_inv_iff.mpr
 
 @[to_additive min_sub_sub_right]
 lemma min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c :=

src/algebra/order/module.lean

@@ -29,7 +29,7 @@ variables {k M N : Type*}
 
 namespace order_dual
 
-instance [semiring k] [ordered_add_comm_monoid M] [module k M] : module k (order_dual M) :=
+instance [semiring k] [ordered_add_comm_monoid M] [module k M] : module k Mᵒᵈ :=
 { add_smul := λ r s x, order_dual.rec (add_smul _ _) x,
   zero_smul := λ m, order_dual.rec (zero_smul _) m }
 
@@ -110,7 +110,7 @@ calc
   ... = 0 : smul_zero' M c
 
 lemma smul_nonneg_of_nonpos_of_nonpos (hc : c ≤ 0) (ha : a ≤ 0) : 0 ≤ c • a :=
-@smul_nonpos_of_nonpos_of_nonneg k (order_dual M) _ _ _ _ _ _ hc ha
+@smul_nonpos_of_nonpos_of_nonneg k Mᵒᵈ _ _ _ _ _ _ hc ha
 
 alias smul_pos_iff_of_neg ↔ _ smul_pos_of_neg_of_neg
 alias smul_neg_iff_of_pos ↔ _ smul_neg_of_pos_of_neg
@@ -149,7 +149,7 @@ end
 variables (M)
 
 /-- Left scalar multiplication as an order isomorphism. -/
-@[simps] def order_iso.smul_left_dual {c : k} (hc : c < 0) : M ≃o order_dual M :=
+@[simps] def order_iso.smul_left_dual {c : k} (hc : c < 0) : M ≃o Mᵒᵈ :=
 { to_fun := λ b, order_dual.to_dual (c • b),
   inv_fun := λ b, c⁻¹ • (order_dual.of_dual b),
   left_inv := inv_smul_smul₀ hc.ne,