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

theorem Finsupp.sum_le_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [OrderedAddCommMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} {h₂ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) : f.sum h₁ ≤ f.sum h₂

instance Finsupp.instLEFinsupp {ι : Type u_1} {α : Type u_3} [Zero α] [LE α] : LE (ι →₀ α)

Equations

• Finsupp.instLEFinsupp = { le := fun (f g : ι →₀ α) => ∀ (i : ι), f i ≤ g i }

theorem Finsupp.le_def {ι : Type u_1} {α : Type u_3} [Zero α] [LE α] {f : ι →₀ α} {g : ι →₀ α} : f ≤ g ↔ ∀ (i : ι), f i ≤ g i

@[simp]

theorem Finsupp.coe_le_coe {ι : Type u_1} {α : Type u_3} [Zero α] [LE α] {f : ι →₀ α} {g : ι →₀ α} : ⇑f ≤ ⇑g ↔ f ≤ g

def Finsupp.orderEmbeddingToFun {ι : Type u_1} {α : Type u_3} [Zero α] [LE α] : (ι →₀ α) ↪o (ι → α)

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

Equations

• Finsupp.orderEmbeddingToFun = { toFun := fun (f : ι →₀ α) => ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Finsupp.orderEmbeddingToFun_apply {ι : Type u_1} {α : Type u_3} [Zero α] [LE α] {f : ι →₀ α} {i : ι} : Finsupp.orderEmbeddingToFun f i = f i

instance Finsupp.preorder {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] : Preorder (ι →₀ α)

Equations

• Finsupp.preorder = Preorder.mk ⋯ ⋯ ⋯

theorem Finsupp.lt_def {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {f : ι →₀ α} {g : ι →₀ α} : f < g ↔ f ≤ g ∧ ∃ (i : ι), f i < g i

@[simp]

theorem Finsupp.coe_lt_coe {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {f : ι →₀ α} {g : ι →₀ α} : ⇑f < ⇑g ↔ f < g

theorem Finsupp.coe_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] : Monotone Finsupp.toFun

theorem Finsupp.coe_strictMono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] : Monotone Finsupp.toFun

@[simp]

theorem Finsupp.single_le_single {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} {b : α} : Finsupp.single i a ≤ Finsupp.single i b ↔ a ≤ b

theorem Finsupp.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} : Monotone (Finsupp.single i)

theorem Finsupp.GCongr.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} {b : α} : a ≤ b → Finsupp.single i a ≤ Finsupp.single i b

Alias of the reverse direction of Finsupp.single_le_single.

@[simp]

theorem Finsupp.single_nonneg {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} : 0 ≤ Finsupp.single i a ↔ 0 ≤ a

@[simp]

theorem Finsupp.single_nonpos {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} : Finsupp.single i a ≤ 0 ↔ a ≤ 0

theorem Finsupp.sum_le_sum_index {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [OrderedAddCommMonoid β] [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

instance Finsupp.partialorder {ι : Type u_1} {α : Type u_3} [Zero α] [PartialOrder α] : PartialOrder (ι →₀ α)

Equations

• Finsupp.partialorder = PartialOrder.mk ⋯

instance Finsupp.semilatticeInf {ι : Type u_1} {α : Type u_3} [Zero α] [SemilatticeInf α] : SemilatticeInf (ι →₀ α)

Equations

• Finsupp.semilatticeInf = SemilatticeInf.mk ⋯ ⋯ ⋯

@[simp]

theorem Finsupp.inf_apply {ι : Type u_1} {α : Type u_3} [Zero α] [SemilatticeInf α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} : (f ⊓ g) i = f i ⊓ g i

instance Finsupp.semilatticeSup {ι : Type u_1} {α : Type u_3} [Zero α] [SemilatticeSup α] : SemilatticeSup (ι →₀ α)

Equations

• Finsupp.semilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

@[simp]

theorem Finsupp.sup_apply {ι : Type u_1} {α : Type u_3} [Zero α] [SemilatticeSup α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} : (f ⊔ g) i = f i ⊔ g i

instance Finsupp.lattice {ι : Type u_1} {α : Type u_3} [Zero α] [Lattice α] : Lattice (ι →₀ α)

Equations

• Finsupp.lattice = Lattice.mk ⋯ ⋯ ⋯

theorem Finsupp.support_inf_union_support_sup {ι : Type u_1} {α : Type u_3} [Zero α] [DecidableEq ι] [Lattice α] (f : ι →₀ α) (g : ι →₀ α) : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support

theorem Finsupp.support_sup_union_support_inf {ι : Type u_1} {α : Type u_3} [Zero α] [DecidableEq ι] [Lattice α] (f : ι →₀ α) (g : ι →₀ α) : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support

Algebraic order structures

instance Finsupp.orderedAddCommMonoid {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] : OrderedAddCommMonoid (ι →₀ α)

Equations

• Finsupp.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

theorem Finsupp.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ι → κ} : Monotone (Finsupp.mapDomain f)

theorem Finsupp.GCongr.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ι → κ} {g₁ : ι →₀ α} {g₂ : ι →₀ α} (hg : g₁ ≤ g₂) : Finsupp.mapDomain f g₁ ≤ Finsupp.mapDomain f g₂

theorem Finsupp.mapDomain_nonneg {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : 0 ≤ g) : 0 ≤ Finsupp.mapDomain f g

theorem Finsupp.mapDomain_nonpos {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : g ≤ 0) : Finsupp.mapDomain f g ≤ 0

instance Finsupp.orderedCancelAddCommMonoid {ι : Type u_1} {α : Type u_3} [OrderedCancelAddCommMonoid α] : OrderedCancelAddCommMonoid (ι →₀ α)

Equations

• Finsupp.orderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Finsupp.contravariantClass {ι : Type u_1} {α : Type u_3} [OrderedAddCommMonoid α] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : ContravariantClass (ι →₀ α) (ι →₀ α) (fun (x1 x2 : ι →₀ α) => x1 + x2) fun (x1 x2 : ι →₀ α) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance Finsupp.instPosSMulMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulMono α β] : PosSMulMono α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instSMulPosMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosMono α β] : SMulPosMono α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instPosSMulReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulReflectLE α β] : PosSMulReflectLE α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instSMulPosReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosReflectLE α β] : SMulPosReflectLE α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instPosSMulStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [PosSMulStrictMono α β] : PosSMulStrictMono α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instSMulPosStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosStrictMono α β] : SMulPosStrictMono α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.instSMulPosReflectLT {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosReflectLT α β] : SMulPosReflectLT α (ι →₀ β)

Equations

• ⋯ = ⋯

instance Finsupp.orderBot {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] : OrderBot (ι →₀ α)

Equations

• Finsupp.orderBot = OrderBot.mk ⋯

theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] : ⊥ = 0

@[simp]

theorem Finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] (f : ι →₀ α) (g : ι →₀ α) : f + g = 0 ↔ f = 0 ∧ g = 0

theorem Finsupp.le_iff' {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] (f : ι →₀ α) (g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

theorem Finsupp.le_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] (f : ι →₀ α) (g : ι →₀ α) : f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i

theorem Finsupp.support_monotone {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] : Monotone Finsupp.support

theorem Finsupp.support_mono {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] {f : ι →₀ α} {g : ι →₀ α} (hfg : f ≤ g) : f.support ⊆ g.support

instance Finsupp.decidableLE {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [DecidableRel LE.le] : DecidableRel LE.le

Equations

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

instance Finsupp.decidableLT {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [DecidableRel LE.le] : DecidableRel LT.lt

Equations

• Finsupp.decidableLT = decidableLTOfDecidableLE

@[simp]

theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] {i : ι} {x : α} {f : ι →₀ α} : Finsupp.single i x ≤ f ↔ x ≤ f i

instance Finsupp.tsub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [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) ⋯ }

instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] : OrderedSub (ι →₀ α)

Equations

• ⋯ = ⋯

instance Finsupp.instCanonicallyOrderedAddCommMonoid {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] : CanonicallyOrderedAddCommMonoid (ι →₀ α)

Equations

• Finsupp.instCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

@[simp]

theorem Finsupp.coe_tsub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) : ⇑(f - g) = ⇑f - ⇑g

theorem Finsupp.tsub_apply {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) (a : ι) : (f - g) a = f a - g a

@[simp]

theorem Finsupp.single_tsub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {i : ι} {a : α} {b : α} : Finsupp.single i (a - b) = Finsupp.single i a - Finsupp.single i b

theorem Finsupp.support_tsub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] {f1 : ι →₀ α} {f2 : ι →₀ α} : (f1 - f2).support ⊆ f1.support

theorem Finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [DecidableEq ι] {f1 : ι →₀ α} {f2 : ι →₀ α} : f1.support \ f2.support ⊆ (f1 - f2).support

@[simp]

theorem Finsupp.support_inf {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedAddCommMonoid α] [DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) : (f ⊓ g).support = f.support ∩ g.support

@[simp]

theorem Finsupp.support_sup {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedAddCommMonoid α] [DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) : (f ⊔ g).support = f.support ∪ g.support

theorem Finsupp.disjoint_iff {ι : Type u_1} {α : Type u_3} [CanonicallyLinearOrderedAddCommMonoid α] {f : ι →₀ α} {g : ι →₀ α} : Disjoint f g ↔ Disjoint f.support g.support

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