[Merged by Bors] - feat: port Algebra.Order.Pointwise

Mathlib.lean

@@ -113,6 +113,7 @@ import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Algebra.Order.Monoid.WithZero.Defs
 import Mathlib.Algebra.Order.Pi
+import Mathlib.Algebra.Order.Pointwise
 import Mathlib.Algebra.Order.Positive.Field
 import Mathlib.Algebra.Order.Positive.Ring
 import Mathlib.Algebra.Order.Ring.Abs

Mathlib/Algebra/Order/Pointwise.lean

@@ -0,0 +1,298 @@
+/-
+Copyright (c) 2021 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best, Yaël Dillies
+
+! This file was ported from Lean 3 source module algebra.order.pointwise
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Bounds
+import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.Order.Field.Defs
+import Mathlib.Data.Set.Pointwise.SMul
+
+/-!
+# Pointwise operations on ordered algebraic objects
+
+This file contains lemmas about the effect of pointwise operations on sets with an order structure.
+
+## TODO
+
+`Sup (s • t) = Sup s • Sup t` and `Inf (s • t) = Inf s • Inf t` hold as well but
+`covariant_class` is currently not polymorphic enough to state it.
+-/
+
+
+open Function Set
+
+open Pointwise
+
+variable {α : Type _}
+
+section ConditionallyCompleteLattice
+
+variable [ConditionallyCompleteLattice α]
+
+section One
+
+variable [One α]
+
+-- Porting note: Use something like `@[to_additive (attr := simp)]` instead.
+-- However, this makes a simpNF error like:
+--  `csupₛ_one` can be proved like `by simp only [csupₛ_zero]
+-- So the `simp` attribute is written below the definition.
+@[to_additive]
+theorem csupₛ_one : supₛ (1 : Set α) = 1 :=
+  csupₛ_singleton _
+#align csupₛ_one csupₛ_one
+
+@[to_additive]
+theorem cinfₛ_one : infₛ (1 : Set α) = 1 :=
+  cinfₛ_singleton _
+#align cinfₛ_one cinfₛ_one
+
+end One
+
+section Group
+
+variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+  {s t : Set α}
+
+-- Porting note: Fix names such as
+-- cSup → csupₛ
+-- cInf → cinfₛ
+@[to_additive]
+theorem csupₛ_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : supₛ s⁻¹ = (infₛ s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv α).map_cinfₛ' hs₀ hs₁).symm
+#align csupₛ_inv csupₛ_inv
+
+@[to_additive]
+theorem cinfₛ_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : infₛ s⁻¹ = (supₛ s)⁻¹ := by
+  rw [← image_inv]
+  exact ((OrderIso.inv α).map_csupₛ' hs₀ hs₁).symm
+#align cinfₛ_inv cinfₛ_inv
+
+@[to_additive]
+theorem csupₛ_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    supₛ (s * t) = supₛ s * supₛ t :=
+  csupₛ_image2_eq_csupₛ_csupₛ (fun _ => (OrderIso.mulRight _).to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+#align csupₛ_mul csupₛ_mul
+
+@[to_additive]
+theorem cinfₛ_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    infₛ (s * t) = infₛ s * infₛ t :=
+  cinfₛ_image2_eq_cinfₛ_cinfₛ (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
+    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁
+#align cinfₛ_mul cinfₛ_mul
+
+@[to_additive]
+theorem csupₛ_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
+    supₛ (s / t) = supₛ s / infₛ t := by
+  rw [div_eq_mul_inv, csupₛ_mul hs₀ hs₁ ht₀.inv ht₁.inv, csupₛ_inv ht₀ ht₁, div_eq_mul_inv]
+#align csupₛ_div csupₛ_div
+
+@[to_additive]
+theorem cinfₛ_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
+    infₛ (s / t) = infₛ s / supₛ t := by
+  rw [div_eq_mul_inv, cinfₛ_mul hs₀ hs₁ ht₀.inv ht₁.inv, cinfₛ_inv ht₀ ht₁, div_eq_mul_inv]
+#align cinfₛ_div cinfₛ_div
+
+end Group
+
+end ConditionallyCompleteLattice
+
+section CompleteLattice
+
+variable [CompleteLattice α]
+
+section One
+
+variable [One α]
+
+-- Porting note: Use something like `@[to_additive (attr := simp)]` instead.
+-- However, this makes a simpNF error like:
+--  `supₛ_one` can be proved like `by simp only [@supₛ_zero]
+-- So the `simp` attribute is written below the definition.
+@[to_additive]
+theorem supₛ_one : supₛ (1 : Set α) = 1 :=
+  supₛ_singleton
+#align Sup_one supₛ_one
+
+@[to_additive]
+theorem infₛ_one : infₛ (1 : Set α) = 1 :=
+  infₛ_singleton
+#align Inf_one infₛ_one
+
+attribute [simp] supₛ_zero
+attribute [simp] infₛ_zero
+attribute [simp] supₛ_one
+attribute [simp] infₛ_one
+attribute [simp] csupₛ_zero
+attribute [simp] cinfₛ_zero
+attribute [simp 900] csupₛ_one
+attribute [simp 900] cinfₛ_one
+
+end One
+
+section Group
+
+variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+  (s t : Set α)
+
+@[to_additive]
+theorem supₛ_inv (s : Set α) : supₛ s⁻¹ = (infₛ s)⁻¹ := by
+  rw [← image_inv, supₛ_image]
+  exact ((OrderIso.inv α).map_infₛ _).symm
+#align Sup_inv supₛ_inv
+
+@[to_additive]
+theorem infₛ_inv (s : Set α) : infₛ s⁻¹ = (supₛ s)⁻¹ := by
+  rw [← image_inv, infₛ_image]
+  exact ((OrderIso.inv α).map_supₛ _).symm
+#align Inf_inv infₛ_inv
+
+@[to_additive]
+theorem supₛ_mul : supₛ (s * t) = supₛ s * supₛ t :=
+  (supₛ_image2_eq_supₛ_supₛ fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).to_galoisConnection
+#align Sup_mul supₛ_mul
+
+@[to_additive]
+theorem infₛ_mul : infₛ (s * t) = infₛ s * infₛ t :=
+  (infₛ_image2_eq_infₛ_infₛ fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
+    (OrderIso.mulLeft _).symm.to_galoisConnection
+#align Inf_mul infₛ_mul
+
+@[to_additive]
+theorem supₛ_div : supₛ (s / t) = supₛ s / infₛ t := by simp_rw [div_eq_mul_inv, supₛ_mul, supₛ_inv]
+#align Sup_div supₛ_div
+
+@[to_additive]
+theorem infₛ_div : infₛ (s / t) = infₛ s / supₛ t := by simp_rw [div_eq_mul_inv, infₛ_mul, infₛ_inv]
+#align Inf_div infₛ_div
+
+end Group
+
+end CompleteLattice
+
+namespace LinearOrderedField
+
+variable {K : Type _} [LinearOrderedField K] {a b r : K} (hr : 0 < r)
+
+open Set
+
+-- Porting note: Removing `include hr`
+
+theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    exact (mul_lt_mul_left hr).mpr a_h_left_left
+    exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
+    rw [mul_div_cancel' _ (ne_of_gt hr)]
+#align linear_ordered_field.smul_Ioo LinearOrderedField.smul_Ioo
+
+theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Icc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    exact (mul_le_mul_left hr).mpr a_h_left_left
+    exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
+    rw [mul_div_cancel' _ (ne_of_gt hr)]
+#align linear_ordered_field.smul_Icc LinearOrderedField.smul_Icc
+
+theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ico]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    exact (mul_le_mul_left hr).mpr a_h_left_left
+    exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine' ⟨⟨(le_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, _⟩
+    rw [mul_div_cancel' _ (ne_of_gt hr)]
+#align linear_ordered_field.smul_Ico LinearOrderedField.smul_Ico
+
+theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    exact (mul_lt_mul_left hr).mpr a_h_left_left
+    exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine' ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff' hr).mpr a_right⟩, _⟩
+    rw [mul_div_cancel' _ (ne_of_gt hr)]
+#align linear_ordered_field.smul_Ioc LinearOrderedField.smul_Ioc
+
+theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    exact (lt_div_iff' hr).mpr h
+    exact mul_div_cancel' _ (ne_of_gt hr)
+#align linear_ordered_field.smul_Ioi LinearOrderedField.smul_Ioi
+
+theorem smul_Iio : r • Iio a = Iio (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    exact (div_lt_iff' hr).mpr h
+    exact mul_div_cancel' _ (ne_of_gt hr)
+#align linear_ordered_field.smul_Iio LinearOrderedField.smul_Iio
+
+theorem smul_Ici : r • Ici a = Ici (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    exact (le_div_iff' hr).mpr h
+    exact mul_div_cancel' _ (ne_of_gt hr)
+#align linear_ordered_field.smul_Ici LinearOrderedField.smul_Ici
+
+theorem smul_Iic : r • Iic a = Iic (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    exact (div_le_iff' hr).mpr h
+    exact mul_div_cancel' _ (ne_of_gt hr)
+#align linear_ordered_field.smul_Iic LinearOrderedField.smul_Iic
+
+end LinearOrderedField