Documentation

Mathlib.Algebra.Order.Pointwise

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 CovariantClass is currently not polymorphic enough to state it.

@[simp]
theorem supₛ_zero {α : Type u_1} [inst : CompleteLattice α] [inst : Zero α] :
supₛ 0 = 0
@[simp]
theorem supₛ_one {α : Type u_1} [inst : CompleteLattice α] [inst : One α] :
supₛ 1 = 1
@[simp]
theorem infₛ_zero {α : Type u_1} [inst : CompleteLattice α] [inst : Zero α] :
infₛ 0 = 0
@[simp]
theorem infₛ_one {α : Type u_1} [inst : CompleteLattice α] [inst : One α] :
infₛ 1 = 1
theorem supₛ_neg {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) :
theorem supₛ_inv {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) :
theorem infₛ_neg {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) :
theorem infₛ_inv {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) :
theorem supₛ_add {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
supₛ (s + t) = supₛ s + supₛ t
theorem supₛ_mul {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
supₛ (s * t) = supₛ s * supₛ t
theorem infₛ_add {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
infₛ (s + t) = infₛ s + infₛ t
theorem infₛ_mul {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
infₛ (s * t) = infₛ s * infₛ t
theorem supₛ_sub {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
supₛ (s - t) = supₛ s - infₛ t
theorem supₛ_div {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
supₛ (s / t) = supₛ s / infₛ t
theorem infₛ_sub {α : Type u_1} [inst : CompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
infₛ (s - t) = infₛ s - supₛ t
theorem infₛ_div {α : Type u_1} [inst : CompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (s : Set α) (t : Set α) :
infₛ (s / t) = infₛ s / supₛ t
@[simp]
theorem csupₛ_zero {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Zero α] :
supₛ 0 = 0
@[simp]
theorem csupₛ_one {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : One α] :
supₛ 1 = 1
@[simp]
theorem cinfₛ_zero {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Zero α] :
infₛ 0 = 0
@[simp]
theorem cinfₛ_one {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : One α] :
infₛ 1 = 1
theorem csupₛ_neg {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) :
theorem csupₛ_inv {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) :
theorem cinfₛ_neg {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) :
theorem cinfₛ_inv {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) :
theorem csupₛ_add {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) (ht₀ : Set.Nonempty t) (ht₁ : BddAbove t) :
supₛ (s + t) = supₛ s + supₛ t
theorem csupₛ_mul {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) (ht₀ : Set.Nonempty t) (ht₁ : BddAbove t) :
supₛ (s * t) = supₛ s * supₛ t
theorem cinfₛ_add {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) (ht₀ : Set.Nonempty t) (ht₁ : BddBelow t) :
infₛ (s + t) = infₛ s + infₛ t
theorem cinfₛ_mul {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) (ht₀ : Set.Nonempty t) (ht₁ : BddBelow t) :
infₛ (s * t) = infₛ s * infₛ t
theorem csupₛ_sub {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) (ht₀ : Set.Nonempty t) (ht₁ : BddBelow t) :
supₛ (s - t) = supₛ s - infₛ t
theorem csupₛ_div {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddAbove s) (ht₀ : Set.Nonempty t) (ht₁ : BddBelow t) :
supₛ (s / t) = supₛ s / infₛ t
theorem cinfₛ_sub {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : AddGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) (ht₀ : Set.Nonempty t) (ht₁ : BddAbove t) :
infₛ (s - t) = infₛ s - supₛ t
theorem cinfₛ_div {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Group α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {s : Set α} {t : Set α} (hs₀ : Set.Nonempty s) (hs₁ : BddBelow s) (ht₀ : Set.Nonempty t) (ht₁ : BddAbove t) :
infₛ (s / t) = infₛ s / supₛ t
theorem LinearOrderedField.smul_Ioo {K : Type u_1} [inst : LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) :
r Set.Ioo a b = Set.Ioo (r a) (r b)
theorem LinearOrderedField.smul_Icc {K : Type u_1} [inst : LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) :
r Set.Icc a b = Set.Icc (r a) (r b)
theorem LinearOrderedField.smul_Ico {K : Type u_1} [inst : LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) :
r Set.Ico a b = Set.Ico (r a) (r b)
theorem LinearOrderedField.smul_Ioc {K : Type u_1} [inst : LinearOrderedField K] {a : K} {b : K} {r : K} (hr : 0 < r) :
r Set.Ioc a b = Set.Ioc (r a) (r b)
theorem LinearOrderedField.smul_Ioi {K : Type u_1} [inst : LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) :
r Set.Ioi a = Set.Ioi (r a)
theorem LinearOrderedField.smul_Iio {K : Type u_1} [inst : LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) :
r Set.Iio a = Set.Iio (r a)
theorem LinearOrderedField.smul_Ici {K : Type u_1} [inst : LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) :
r Set.Ici a = Set.Ici (r a)
theorem LinearOrderedField.smul_Iic {K : Type u_1} [inst : LinearOrderedField K] {a : K} {r : K} (hr : 0 < r) :
r Set.Iic a = Set.Iic (r a)