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.
@[simp]
@[simp]
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
: