mathlib documentation

data.finsupp.order

Pointwise order on finitely supported functions #

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

Main declarations #

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 α] [partial_order α] :
Equations
@[protected, instance]
noncomputable def finsupp.semilattice_inf {ι : Type u_1} {α : Type u_2} [has_zero α] [semilattice_inf α] :
Equations
@[simp]
theorem finsupp.inf_apply {ι : Type u_1} {α : Type u_2} [has_zero α] [semilattice_inf α] {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 α] [semilattice_sup α] :
Equations
@[simp]
theorem finsupp.sup_apply {ι : Type u_1} {α : Type u_2} [has_zero α] [semilattice_sup α] {i : ι} {f g : ι →₀ α} :
(f g) i = f i g i

Algebraic order structures #

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

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

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

Some lemmas about #

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