# Pointwise order on finitely supported functions #

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

## Main declarations #

- `Finsupp.orderEmbeddingToFun`: The order embedding from finitely supported functions to functions.

### Order structures #

source
theorem Finsupp.sum_le_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ h₂ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) :
f.sum h₁ ≤ f.sum h₂
source
theorem Finsupp.sum_nonneg {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ i ∈ f.support, 0 ≤ h₁ i (f i)) :
0 ≤ f.sum h₁
source
theorem Finsupp.sum_nonneg' {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ (i : ι), 0 ≤ h₁ i (f i)) :
0 ≤ f.sum h₁
source
theorem Finsupp.sum_nonpos {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ 0) :
f.sum h₁ ≤ 0
source
@[simp]
theorem Finsupp.single_le_single {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a b : α} :
single i a ≤ single i b ↔ a ≤ b
source
theorem Finsupp.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} :
Monotone (single i)
source
theorem Finsupp.GCongr.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a b : α} :
a ≤ b → single i a ≤ single i b

Alias of the reverse direction of `Finsupp.single_le_single`.

source
@[simp]
theorem Finsupp.single_nonneg {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} :
0 ≤ single i a ↔ 0 ≤ a
source
@[simp]
theorem Finsupp.single_nonpos {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} :
single i a ≤ 0 ↔ a ≤ 0
source
theorem Finsupp.sum_le_sum_index {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂) (hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) :
f₁.sum h ≤ f₂.sum h

### Algebraic order structures #

source
instance Finsupp.isOrderedAddMonoid {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
IsOrderedAddMonoid (ι →₀ α)
source
theorem Finsupp.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {f : ι → κ} :
Monotone (mapDomain f)
source
theorem Finsupp.mapDomain_nonneg {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : 0 ≤ g) :
0 ≤ mapDomain f g
source
theorem Finsupp.mapDomain_nonpos {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : g ≤ 0) :
mapDomain f g ≤ 0
source
instance Finsupp.isOrderedCancelAddMonoid {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
IsOrderedCancelAddMonoid (ι →₀ α)
source
instance Finsupp.addLeftReflectLE {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddLeftReflectLE α] :
AddLeftReflectLE (ι →₀ α)
source
instance Finsupp.instPosSMulMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulMono α β] :
PosSMulMono α (ι →₀ β)
source
instance Finsupp.instSMulPosMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosMono α β] :
SMulPosMono α (ι →₀ β)
source
instance Finsupp.instPosSMulReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulReflectLE α β] :
PosSMulReflectLE α (ι →₀ β)
source
instance Finsupp.instSMulPosReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosReflectLE α β] :
SMulPosReflectLE α (ι →₀ β)
source
instance Finsupp.instPosSMulStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [PosSMulStrictMono α β] :
PosSMulStrictMono α (ι →₀ β)
source
instance Finsupp.instSMulPosStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosStrictMono α β] :
SMulPosStrictMono α (ι →₀ β)
source
instance Finsupp.instSMulPosReflectLT {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosReflectLT α β] :
SMulPosReflectLT α (ι →₀ β)
source
instance Finsupp.orderBot {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] :
OrderBot (ι →₀ α)
Equations

- Finsupp.orderBot = { bot := 0, bot_le := ⋯ }

source
theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] :
⊥ = 0
source
@[simp]
theorem Finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) :
f + g = 0 ↔ f = 0 ∧ g = 0
source
theorem Finsupp.le_iff' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) :
f ≤ g ↔ ∀ i ∈ s, f i ≤ g i
source
theorem Finsupp.le_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) :
f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
source
theorem Finsupp.support_monotone {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] :
Monotone support
source
theorem Finsupp.support_mono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {f g : ι →₀ α} (hfg : f ≤ g) :
f.support ⊆ g.support
source
instance Finsupp.decidableLE {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [DecidableLE α] :
DecidableLE (ι →₀ α)
Equations

- f.decidableLE g = decidable_of_iff (∀ i ∈ f.support, f i ≤ g i) ⋯

source
instance Finsupp.decidableLT {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [DecidableLE α] :
DecidableLT (ι →₀ α)
Equations

- Finsupp.decidableLT = decidableLTOfDecidableLE

source
@[simp]
theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {i : ι} {x : α} {f : ι →₀ α} :
single i x ≤ f ↔ x ≤ f i
source
instance Finsupp.tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] :
Sub (ι →₀ α)

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

Equations

- Finsupp.tsub = { sub := Finsupp.zipWith (fun (m n : α) => m - n) ⋯ }

source
instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] :
OrderedSub (ι →₀ α)
source
instance Finsupp.instCanonicallyOrderedAddOfAddLeftMono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftMono α] :
CanonicallyOrderedAdd (ι →₀ α)
source
@[simp]
theorem Finsupp.coe_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (f g : ι →₀ α) :
⇑(f - g) = ⇑f - ⇑g
source
theorem Finsupp.tsub_apply {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (f g : ι →₀ α) (a : ι) :
(f - g) a = f a - g a
source
@[simp]
theorem Finsupp.single_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {i : ι} {a b : α} :
single i (a - b) = single i a - single i b
source
theorem Finsupp.support_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {f1 f2 : ι →₀ α} :
(f1 - f2).support ⊆ f1.support
source
theorem Finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [DecidableEq ι] {f1 f2 : ι →₀ α} :
f1.support \ f2.support ⊆ (f1 - f2).support
source
@[simp]
theorem Finsupp.support_inf {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [DecidableEq ι] (f g : ι →₀ α) :
(f ⊓ g).support = f.support ∩ g.support
source
@[simp]
theorem Finsupp.support_sup {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [DecidableEq ι] (f g : ι →₀ α) :
(f ⊔ g).support = f.support ∪ g.support
source
theorem Finsupp.disjoint_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] {f g : ι →₀ α} :
Disjoint f g ↔ Disjoint f.support g.support

### Some lemmas about `ℕ` #

source
theorem Finsupp.sub_single_one_add {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ} (h : u a ≠ 0) :
u - single a 1 + u' = u + u' - single a 1
source
theorem Finsupp.add_sub_single_one {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ} (h : u' a ≠ 0) :
u + (u' - single a 1) = u + u' - single a 1
source
theorem Finsupp.sub_add_single_one_cancel {ι : Type u_1} {u : ι →₀ ℕ} {i : ι} (h : u i ≠ 0) :
u - single i 1 + single i 1 = u