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