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.

source

ink

@[simp]

theorem supₛ_zero {α : Type u_1} [inst : CompleteLattice α] [inst : Zero α] :

supₛ 0 = 0

source

ink

@[simp]

theorem supₛ_one {α : Type u_1} [inst : CompleteLattice α] [inst : One α] :

supₛ 1 = 1

source

ink

@[simp]

theorem infₛ_zero {α : Type u_1} [inst : CompleteLattice α] [inst : Zero α] :

infₛ 0 = 0

source

ink

@[simp]

theorem infₛ_one {α : Type u_1} [inst : CompleteLattice α] [inst : One α] :

infₛ 1 = 1

source

ink

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 α) :

supₛ (-s) = -infₛ s

source

ink

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 α) :

supₛ s⁻¹ = (infₛ s)⁻¹

source

ink

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 α) :

infₛ (-s) = -supₛ s

source

ink

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 α) :

infₛ s⁻¹ = (supₛ s)⁻¹

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

@[simp]

theorem csupₛ_zero {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Zero α] :

supₛ 0 = 0

source

ink

@[simp]

theorem csupₛ_one {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : One α] :

supₛ 1 = 1

source

ink

@[simp]

theorem cinfₛ_zero {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : Zero α] :

infₛ 0 = 0

source

ink

@[simp]

theorem cinfₛ_one {α : Type u_1} [inst : ConditionallyCompleteLattice α] [inst : One α] :

infₛ 1 = 1

source

ink

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) :

supₛ (-s) = -infₛ s

source

ink

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) :

supₛ s⁻¹ = (infₛ s)⁻¹

source

ink

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) :

infₛ (-s) = -supₛ s

source

ink

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) :

infₛ s⁻¹ = (supₛ s)⁻¹

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)

source

ink

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)