Documentation

Mathlib.Data.Finsupp.Order

Pointwise order on finitely supported functions #

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

Main declarations #

Order structures #

theorem Finsupp.sum_le_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [OrderedAddCommMonoid β] {f : ι →₀ α} {h₁ : ιαβ} {h₂ : ιαβ} (h : if.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' := }
Instances For
    @[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 α] :
    Equations
    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 : α} :
    theorem Finsupp.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} :
    theorem Finsupp.GCongr.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} {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 : α} :
    @[simp]
    theorem Finsupp.single_nonpos {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} :
    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 : if₁.support f₂.support, Monotone (h i)) (hh₀ : if₁.support f₂.support, h i 0 = 0) :
    f₁.sum h f₂.sum h
    instance Finsupp.partialorder {ι : Type u_1} {α : Type u_3} [Zero α] [PartialOrder α] :
    Equations
    instance Finsupp.semilatticeInf {ι : Type u_1} {α : Type u_3} [Zero α] [SemilatticeInf α] :
    Equations
    @[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 α] :
    Equations
    @[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
    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 #

    Equations
    theorem Finsupp.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ικ} :
    theorem Finsupp.GCongr.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ικ} {g₁ : ι →₀ α} {g₂ : ι →₀ α} (hg : g₁ g₂) :
    theorem Finsupp.mapDomain_nonneg {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ικ} {g : ι →₀ α} (hg : 0 g) :
    theorem Finsupp.mapDomain_nonpos {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [OrderedAddCommMonoid α] {f : ικ} {g : ι →₀ α} (hg : g 0) :
    Equations
    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 α β] :
    Equations
    • =
    instance Finsupp.instSMulPosReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosReflectLE α β] :
    Equations
    • =
    instance Finsupp.instPosSMulStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [PosSMulStrictMono α β] :
    Equations
    • =
    instance Finsupp.instSMulPosStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosStrictMono α β] :
    Equations
    • =
    instance Finsupp.instSMulPosReflectLT {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosReflectLT α β] :
    Equations
    • =
    instance Finsupp.orderBot {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] :
    Equations
    @[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 is, f i g i
    theorem Finsupp.le_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] (f : ι →₀ α) (g : ι →₀ α) :
    f g if.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] :
    Equations
    instance Finsupp.decidableLT {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [DecidableRel LE.le] :
    Equations
    • Finsupp.decidableLT = decidableLTOfDecidableLE
    @[simp]
    theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] {i : ι} {x : α} {f : ι →₀ α} :
    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
    instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] :
    Equations
    • =
    Equations
    @[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 : α} :
    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