mathlib documentation

algebra.order.pointwise

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 covariant_class is currently not polymorphic enough to state it.

@[simp]
theorem cSup_zero {α : Type u_1} [conditionally_complete_lattice α] [has_zero α] :
@[simp]
theorem cSup_one {α : Type u_1} [conditionally_complete_lattice α] [has_one α] :
@[simp]
theorem cInf_zero {α : Type u_1} [conditionally_complete_lattice α] [has_zero α] :
@[simp]
theorem cInf_one {α : Type u_1} [conditionally_complete_lattice α] [has_one α] :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[simp]
theorem Sup_zero {α : Type u_1} [complete_lattice α] [has_zero α] :
@[simp]
theorem Sup_one {α : Type u_1} [complete_lattice α] [has_one α] :
@[simp]
theorem Inf_zero {α : Type u_1} [complete_lattice α] [has_zero α] :
@[simp]
theorem Inf_one {α : Type u_1} [complete_lattice α] [has_one α] :
theorem linear_ordered_field.smul_Ioo {K : Type u_2} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Ioo a b = set.Ioo (r a) (r b)
theorem linear_ordered_field.smul_Icc {K : Type u_2} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Icc a b = set.Icc (r a) (r b)
theorem linear_ordered_field.smul_Ico {K : Type u_2} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Ico a b = set.Ico (r a) (r b)
theorem linear_ordered_field.smul_Ioc {K : Type u_2} [linear_ordered_field K] {a b r : K} (hr : 0 < r) :
r set.Ioc a b = set.Ioc (r a) (r b)
theorem linear_ordered_field.smul_Ioi {K : Type u_2} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Ioi a = set.Ioi (r a)
theorem linear_ordered_field.smul_Iio {K : Type u_2} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Iio a = set.Iio (r a)
theorem linear_ordered_field.smul_Ici {K : Type u_2} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Ici a = set.Ici (r a)
theorem linear_ordered_field.smul_Iic {K : Type u_2} [linear_ordered_field K] {a r : K} (hr : 0 < r) :
r set.Iic a = set.Iic (r a)