Pointwise order on finitely supported dependent functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file lifts order structures on the α i to Π₀ i, α i.
Main declarations #
dfinsupp.order_embedding_to_fun: The order embedding from finitely supported dependent functions to functions.
Order structures #
def
dfinsupp.order_embedding_to_fun
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_zero (α i)]
[Π (i : ι), has_le (α i)] :
The order on dfinsupps over a partial order embeds into the order on functions
Equations
- dfinsupp.order_embedding_to_fun = {to_embedding := {to_fun := coe_fn dfinsupp.has_coe_to_fun, inj' := _}, map_rel_iff' := _}
@[protected, instance]
def
dfinsupp.partial_order
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_zero (α i)]
[Π (i : ι), partial_order (α i)] :
partial_order (Π₀ (i : ι), α i)
Equations
- dfinsupp.partial_order = {le := preorder.le dfinsupp.preorder, lt := preorder.lt dfinsupp.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
dfinsupp.semilattice_inf
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_zero (α i)]
[Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π₀ (i : ι), α i)
Equations
- dfinsupp.semilattice_inf = {inf := dfinsupp.zip_with (λ (_x : ι), has_inf.inf) dfinsupp.semilattice_inf._proof_1, le := partial_order.le dfinsupp.partial_order, lt := partial_order.lt dfinsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
dfinsupp.semilattice_sup
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_zero (α i)]
[Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π₀ (i : ι), α i)
Equations
- dfinsupp.semilattice_sup = {sup := dfinsupp.zip_with (λ (_x : ι), has_sup.sup) dfinsupp.semilattice_sup._proof_1, le := partial_order.le dfinsupp.partial_order, lt := partial_order.lt dfinsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[protected, instance]
def
dfinsupp.lattice
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_zero (α i)]
[Π (i : ι), lattice (α i)] :
Equations
- dfinsupp.lattice = {sup := semilattice_sup.sup dfinsupp.semilattice_sup, le := semilattice_inf.le dfinsupp.semilattice_inf, lt := semilattice_inf.lt dfinsupp.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf dfinsupp.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
Algebraic order structures #
@[protected, instance]
def
dfinsupp.ordered_add_comm_monoid
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), ordered_add_comm_monoid (α i)] :
ordered_add_comm_monoid (Π₀ (i : ι), α i)
Equations
- dfinsupp.ordered_add_comm_monoid α = {add := add_comm_monoid.add dfinsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero dfinsupp.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul dfinsupp.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le dfinsupp.partial_order, lt := partial_order.lt dfinsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
def
dfinsupp.ordered_cancel_add_comm_monoid
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), ordered_cancel_add_comm_monoid (α i)] :
ordered_cancel_add_comm_monoid (Π₀ (i : ι), α i)
Equations
- dfinsupp.ordered_cancel_add_comm_monoid α = {add := ordered_add_comm_monoid.add (dfinsupp.ordered_add_comm_monoid α), add_assoc := _, zero := ordered_add_comm_monoid.zero (dfinsupp.ordered_add_comm_monoid α), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (dfinsupp.ordered_add_comm_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le (dfinsupp.ordered_add_comm_monoid α), lt := ordered_add_comm_monoid.lt (dfinsupp.ordered_add_comm_monoid α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
def
dfinsupp.has_le.le.contravariant_class
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), ordered_add_comm_monoid (α i)]
[∀ (i : ι), contravariant_class (α i) (α i) has_add.add has_le.le] :
contravariant_class (Π₀ (i : ι), α i) (Π₀ (i : ι), α i) has_add.add has_le.le
@[protected, instance]
def
dfinsupp.order_bot
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), canonically_ordered_add_monoid (α i)] :
Equations
- dfinsupp.order_bot α = {bot := 0, bot_le := _}
@[protected]
theorem
dfinsupp.bot_eq_zero
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), canonically_ordered_add_monoid (α i)] :
@[protected, instance]
def
dfinsupp.decidable_le
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[decidable_eq ι]
[Π (i : ι) (x : α i), decidable (x ≠ 0)]
[Π (i : ι), decidable_rel has_le.le] :
@[simp]
theorem
dfinsupp.single_le_iff
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[decidable_eq ι]
[Π (i : ι) (x : α i), decidable (x ≠ 0)]
{f : Π₀ (i : ι), α i}
{i : ι}
{a : α i} :
dfinsupp.single i a ≤ f ↔ a ≤ ⇑f i
@[protected, instance]
def
dfinsupp.tsub
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[Π (i : ι), has_sub (α i)]
[∀ (i : ι), has_ordered_sub (α i)] :
This is called tsub for truncated subtraction, to distinguish it with subtraction in an
additive group.
Equations
- dfinsupp.tsub α = {sub := dfinsupp.zip_with (λ (i : ι) (m n : α i), m - n) _}
@[protected, instance]
def
dfinsupp.has_ordered_sub
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[Π (i : ι), has_sub (α i)]
[∀ (i : ι), has_ordered_sub (α i)] :
has_ordered_sub (Π₀ (i : ι), α i)
@[protected, instance]
def
dfinsupp.canonically_ordered_add_monoid
{ι : Type u_1}
(α : ι → Type u_2)
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[Π (i : ι), has_sub (α i)]
[∀ (i : ι), has_ordered_sub (α i)] :
canonically_ordered_add_monoid (Π₀ (i : ι), α i)
Equations
- dfinsupp.canonically_ordered_add_monoid α = {add := ordered_add_comm_monoid.add (dfinsupp.ordered_add_comm_monoid α), add_assoc := _, zero := ordered_add_comm_monoid.zero (dfinsupp.ordered_add_comm_monoid α), zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul (dfinsupp.ordered_add_comm_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le (dfinsupp.ordered_add_comm_monoid α), lt := ordered_add_comm_monoid.lt (dfinsupp.ordered_add_comm_monoid α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot (dfinsupp.order_bot α), bot_le := _, exists_add_of_le := _, le_self_add := _}
@[simp]
theorem
dfinsupp.single_tsub
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[Π (i : ι), has_sub (α i)]
[∀ (i : ι), has_ordered_sub (α i)]
{i : ι}
{a b : α i}
[decidable_eq ι] :
dfinsupp.single i (a - b) = dfinsupp.single i a - dfinsupp.single i b
theorem
dfinsupp.subset_support_tsub
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), canonically_ordered_add_monoid (α i)]
[Π (i : ι), has_sub (α i)]
[∀ (i : ι), has_ordered_sub (α i)]
{f g : Π₀ (i : ι), α i}
[decidable_eq ι]
[Π (i : ι) (x : α i), decidable (x ≠ 0)] :
theorem
dfinsupp.disjoint_iff
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), canonically_linear_ordered_add_monoid (α i)]
[decidable_eq ι]
{f g : Π₀ (i : ι), α i} :