# mathlibdocumentation

data.finsupp.order

# Pointwise order on finitely supported functions #

This file lifts order structures on α to ι →₀ α.

## Main declarations #

• finsupp.order_embedding_to_fun: The order embedding from finitely supported functions to functions.
• finsupp.order_iso_multiset: The order isomorphism between ℕ-valued finitely supported functions and multisets.

### Order structures #

@[protected, instance]
def finsupp.has_le {ι : Type u_1} {α : Type u_2} [has_zero α] [has_le α] :
has_le →₀ α)
Equations
theorem finsupp.le_def {ι : Type u_1} {α : Type u_2} [has_zero α] [has_le α] {f g : ι →₀ α} :
f g ∀ (i : ι), f i g i
def finsupp.order_embedding_to_fun {ι : Type u_1} {α : Type u_2} [has_zero α] [has_le α] :
→₀ α) ↪o (ι → α)

The order on finsupps over a partial order embeds into the order on functions

Equations
@[simp]
theorem finsupp.order_embedding_to_fun_apply {ι : Type u_1} {α : Type u_2} [has_zero α] [has_le α] {f : ι →₀ α} {i : ι} :
@[protected, instance]
def finsupp.preorder {ι : Type u_1} {α : Type u_2} [has_zero α] [preorder α] :
Equations
theorem finsupp.monotone_to_fun {ι : Type u_1} {α : Type u_2} [has_zero α] [preorder α] :
@[protected, instance]
def finsupp.partial_order {ι : Type u_1} {α : Type u_2} [has_zero α]  :
Equations
@[protected, instance]
noncomputable def finsupp.semilattice_inf {ι : Type u_1} {α : Type u_2} [has_zero α]  :
Equations
@[simp]
theorem finsupp.inf_apply {ι : Type u_1} {α : Type u_2} [has_zero α] {i : ι} {f g : ι →₀ α} :
(f g) i = f i g i
@[protected, instance]
noncomputable def finsupp.semilattice_sup {ι : Type u_1} {α : Type u_2} [has_zero α]  :
Equations
@[simp]
theorem finsupp.sup_apply {ι : Type u_1} {α : Type u_2} [has_zero α] {i : ι} {f g : ι →₀ α} :
(f g) i = f i g i
@[protected, instance]
noncomputable def finsupp.lattice {ι : Type u_1} {α : Type u_2} [has_zero α] [lattice α] :
lattice →₀ α)
Equations

### Algebraic order structures #

@[protected, instance]
noncomputable def finsupp.ordered_add_comm_monoid {ι : Type u_1} {α : Type u_2}  :
Equations
@[protected, instance]
noncomputable def finsupp.ordered_cancel_add_comm_monoid {ι : Type u_1} {α : Type u_2}  :
Equations
@[protected, instance]
def finsupp.has_le.le.contravariant_class {ι : Type u_1} {α : Type u_2}  :
@[protected, instance]
def finsupp.order_bot {ι : Type u_1} {α : Type u_2}  :
Equations
@[protected]
theorem finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_2}  :
= 0
@[simp]
theorem finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_2} (f g : ι →₀ α) :
f + g = 0 f = 0 g = 0
theorem finsupp.le_iff' {ι : Type u_1} {α : Type u_2} (f g : ι →₀ α) {s : finset ι} (hf : f.support s) :
f g ∀ (i : ι), i sf i g i
theorem finsupp.le_iff {ι : Type u_1} {α : Type u_2} (f g : ι →₀ α) :
f g ∀ (i : ι), i f.supportf i g i
@[protected, instance]
def finsupp.decidable_le {ι : Type u_1} {α : Type u_2}  :
Equations
@[simp]
theorem finsupp.single_le_iff {ι : Type u_1} {α : Type u_2} {i : ι} {x : α} {f : ι →₀ α} :
f x f i
@[protected, instance]
noncomputable def finsupp.tsub {ι : Type u_1} {α : Type u_2} [has_sub α]  :
has_sub →₀ α)

This is called tsub for truncated subtraction, to distinguish it with subtraction in an additive group.

Equations
@[protected, instance]
def finsupp.has_ordered_sub {ι : Type u_1} {α : Type u_2} [has_sub α]  :
Equations
@[protected, instance]
noncomputable def finsupp.canonically_ordered_add_monoid {ι : Type u_1} {α : Type u_2} [has_sub α]  :
Equations
@[simp]
theorem finsupp.coe_tsub {ι : Type u_1} {α : Type u_2} [has_sub α] (f g : ι →₀ α) :
(f - g) = f - g
theorem finsupp.tsub_apply {ι : Type u_1} {α : Type u_2} [has_sub α] (f g : ι →₀ α) (a : ι) :
(f - g) a = f a - g a
@[simp]
theorem finsupp.single_tsub {ι : Type u_1} {α : Type u_2} [has_sub α] {i : ι} {a b : α} :
(a - b) = -
theorem finsupp.support_tsub {ι : Type u_1} {α : Type u_2} [has_sub α] {f1 f2 : ι →₀ α} :
(f1 - f2).support f1.support
theorem finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_2} [has_sub α] {f1 f2 : ι →₀ α} :
f1.support \ f2.support (f1 - f2).support
@[simp]
theorem finsupp.support_inf {ι : Type u_1} {α : Type u_2} [decidable_eq ι] {f g : ι →₀ α} :
@[simp]
theorem finsupp.support_sup {ι : Type u_1} {α : Type u_2} [decidable_eq ι] {f g : ι →₀ α} :
theorem finsupp.disjoint_iff {ι : Type u_1} {α : Type u_2} [decidable_eq ι] {f g : ι →₀ α} :
g

### Some lemmas about ℕ#

theorem finsupp.sub_single_one_add {ι : Type u_1} {a : ι} {u u' : ι →₀ } (h : u a 0) :
u - + u' = u + u' -
theorem finsupp.add_sub_single_one {ι : Type u_1} {a : ι} {u u' : ι →₀ } (h : u' a 0) :
u + (u' - 1) = u + u' -