Pointwise operations on ordered algebraic objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
covariant_class is currently not polymorphic enough to state it.
@[simp]
theorem
cSup_zero
{α : Type u_1}
[conditionally_complete_lattice α]
[has_zero α] :
has_Sup.Sup 0 = 0
@[simp]
@[simp]
theorem
cInf_zero
{α : Type u_1}
[conditionally_complete_lattice α]
[has_zero α] :
has_Inf.Inf 0 = 0
@[simp]
theorem
cSup_inv
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s) :
has_Sup.Sup s⁻¹ = (has_Inf.Inf s)⁻¹
theorem
cSup_neg
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s) :
has_Sup.Sup (-s) = -has_Inf.Inf s
theorem
cInf_neg
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s) :
has_Inf.Inf (-s) = -has_Sup.Sup s
theorem
cInf_inv
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s) :
has_Inf.Inf s⁻¹ = (has_Sup.Sup s)⁻¹
theorem
cSup_add
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s)
(ht₀ : t.nonempty)
(ht₁ : bdd_above t) :
has_Sup.Sup (s + t) = has_Sup.Sup s + has_Sup.Sup t
theorem
cSup_mul
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s)
(ht₀ : t.nonempty)
(ht₁ : bdd_above t) :
has_Sup.Sup (s * t) = has_Sup.Sup s * has_Sup.Sup t
theorem
cInf_mul
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s)
(ht₀ : t.nonempty)
(ht₁ : bdd_below t) :
has_Inf.Inf (s * t) = has_Inf.Inf s * has_Inf.Inf t
theorem
cInf_add
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s)
(ht₀ : t.nonempty)
(ht₁ : bdd_below t) :
has_Inf.Inf (s + t) = has_Inf.Inf s + has_Inf.Inf t
theorem
cSup_div
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s)
(ht₀ : t.nonempty)
(ht₁ : bdd_below t) :
has_Sup.Sup (s / t) = has_Sup.Sup s / has_Inf.Inf t
theorem
cSup_sub
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_above s)
(ht₀ : t.nonempty)
(ht₁ : bdd_below t) :
has_Sup.Sup (s - t) = has_Sup.Sup s - has_Inf.Inf t
theorem
cInf_sub
{α : Type u_1}
[conditionally_complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s)
(ht₀ : t.nonempty)
(ht₁ : bdd_above t) :
has_Inf.Inf (s - t) = has_Inf.Inf s - has_Sup.Sup t
theorem
cInf_div
{α : Type u_1}
[conditionally_complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{s t : set α}
(hs₀ : s.nonempty)
(hs₁ : bdd_below s)
(ht₀ : t.nonempty)
(ht₁ : bdd_above t) :
has_Inf.Inf (s / t) = has_Inf.Inf s / has_Sup.Sup t
@[simp]
@[simp]
theorem
Sup_neg
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : set α) :
has_Sup.Sup (-s) = -has_Inf.Inf s
theorem
Sup_inv
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : set α) :
has_Sup.Sup s⁻¹ = (has_Inf.Inf s)⁻¹
theorem
Inf_neg
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : set α) :
has_Inf.Inf (-s) = -has_Sup.Sup s
theorem
Inf_inv
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : set α) :
has_Inf.Inf s⁻¹ = (has_Sup.Sup s)⁻¹
theorem
Sup_mul
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : set α) :
has_Sup.Sup (s * t) = has_Sup.Sup s * has_Sup.Sup t
theorem
Sup_add
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : set α) :
has_Sup.Sup (s + t) = has_Sup.Sup s + has_Sup.Sup t
theorem
Inf_add
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : set α) :
has_Inf.Inf (s + t) = has_Inf.Inf s + has_Inf.Inf t
theorem
Inf_mul
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : set α) :
has_Inf.Inf (s * t) = has_Inf.Inf s * has_Inf.Inf t
theorem
Sup_div
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : set α) :
has_Sup.Sup (s / t) = has_Sup.Sup s / has_Inf.Inf t
theorem
Sup_sub
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : set α) :
has_Sup.Sup (s - t) = has_Sup.Sup s - has_Inf.Inf t
theorem
Inf_div
{α : Type u_1}
[complete_lattice α]
[group α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : set α) :
has_Inf.Inf (s / t) = has_Inf.Inf s / has_Sup.Sup t
theorem
Inf_sub
{α : Type u_1}
[complete_lattice α]
[add_group α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : set α) :
has_Inf.Inf (s - t) = has_Inf.Inf s - has_Sup.Sup t
theorem
linear_ordered_field.smul_Ioi
{K : Type u_2}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Iio
{K : Type u_2}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Ici
{K : Type u_2}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :
theorem
linear_ordered_field.smul_Iic
{K : Type u_2}
[linear_ordered_field K]
{a r : K}
(hr : 0 < r) :