Documentation

Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Infima/suprema in ordered monoids and groups #

In this file we prove a few facts like “The infimum of -s is - the supremum of s”.

TODO #

sSup (s • t) = sSup s • sSup t and sInf (s • t) = sInf s • sInf t hold as well but CovariantClass is currently not polymorphic enough to state it.

source
@[simp]
theorem csSup_zero {M : Type u_3} [ConditionallyCompleteLattice M] [Zero M] :
sSup 0 = 0
source
@[simp]
theorem csSup_one {M : Type u_3} [ConditionallyCompleteLattice M] [One M] :
sSup 1 = 1
source
@[simp]
theorem csInf_zero {M : Type u_3} [ConditionallyCompleteLattice M] [Zero M] :
sInf 0 = 0
source
@[simp]
theorem csInf_one {M : Type u_3} [ConditionallyCompleteLattice M] [One M] :
sInf 1 = 1
source
theorem csSup_neg {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) :
sSup (-s) = -sInf s
source
theorem csSup_inv {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) :
sSup s⁻¹ = (sInf s)⁻¹
source
theorem csInf_neg {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) :
sInf (-s) = -sSup s
source
theorem csInf_inv {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) :
sInf s⁻¹ = (sSup s)⁻¹
source
theorem csSup_add {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
sSup (s + t) = sSup s + sSup t
source
theorem csSup_mul {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
sSup (s * t) = sSup s * sSup t
source
theorem csInf_add {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
sInf (s + t) = sInf s + sInf t
source
theorem csInf_mul {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
sInf (s * t) = sInf s * sInf t
source
theorem csSup_sub {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
sSup (s - t) = sSup s - sInf t
source
theorem csSup_div {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) :
sSup (s / t) = sSup s / sInf t
source
theorem csInf_sub {M : Type u_3} [ConditionallyCompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
sInf (s - t) = sInf s - sSup t
source
theorem csInf_div {M : Type u_3} [ConditionallyCompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] {s : Set M} {t : Set M} (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :
sInf (s / t) = sInf s / sSup t
source
theorem sSup_zero {M : Type u_3} [CompleteLattice M] [Zero M] :
sSup 0 = 0
source
theorem sSup_one {M : Type u_3} [CompleteLattice M] [One M] :
sSup 1 = 1
source
theorem sInf_zero {M : Type u_3} [CompleteLattice M] [Zero M] :
sInf 0 = 0
source
theorem sInf_one {M : Type u_3} [CompleteLattice M] [One M] :
sInf 1 = 1
source
theorem sSup_neg {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) :
sSup (-s) = -sInf s
source
theorem sSup_inv {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) :
sSup s⁻¹ = (sInf s)⁻¹
source
theorem sInf_neg {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) :
sInf (-s) = -sSup s
source
theorem sInf_inv {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) :
sInf s⁻¹ = (sSup s)⁻¹
source
theorem sSup_add {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sSup (s + t) = sSup s + sSup t
source
theorem sSup_mul {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sSup (s * t) = sSup s * sSup t
source
theorem sInf_add {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sInf (s + t) = sInf s + sInf t
source
theorem sInf_mul {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sInf (s * t) = sInf s * sInf t
source
theorem sSup_sub {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sSup (s - t) = sSup s - sInf t
source
theorem sSup_div {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sSup (s / t) = sSup s / sInf t
source
theorem sInf_sub {M : Type u_3} [CompleteLattice M] [AddGroup M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sInf (s - t) = sInf s - sSup t
source
theorem sInf_div {M : Type u_3} [CompleteLattice M] [Group M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2] (s : Set M) (t : Set M) :
sInf (s / t) = sInf s / sSup t