Documentation

Mathlib.Data.Finsupp.Order

Pointwise order on finitely supported functions #

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

Main declarations #

Order structures #

instance Finsupp.instLEFinsupp {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : LE α] :
LE (ι →₀ α)
Equations
  • Finsupp.instLEFinsupp = { le := fun f g => ∀ (i : ι), f i g i }
theorem Finsupp.le_def {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : LE α] {f : ι →₀ α} {g : ι →₀ α} :
f g ∀ (i : ι), f i g i
def Finsupp.orderEmbeddingToFun {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : LE α] :
(ι →₀ α) ↪o (ια)

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finsupp.orderEmbeddingToFun_apply {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : LE α] {f : ι →₀ α} {i : ι} :
Finsupp.orderEmbeddingToFun.toEmbedding f i = f i
instance Finsupp.preorder {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : Preorder α] :
Equations
  • Finsupp.preorder = let src := Finsupp.instLEFinsupp; Preorder.mk (_ : ∀ (f : ι →₀ α) (i : ι), f i f i) (_ : ∀ (f g h : ι →₀ α), f gg h∀ (i : ι), f i h i)
theorem Finsupp.monotone_toFun {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : Preorder α] :
Monotone Finsupp.toFun
instance Finsupp.partialorder {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : PartialOrder α] :
Equations
instance Finsupp.semilatticeInf {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : SemilatticeInf α] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finsupp.inf_apply {ι : Type u_2} {α : Type u_1} [inst : Zero α] [inst : SemilatticeInf α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} :
↑(f g) i = f i g i
instance Finsupp.semilatticeSup {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : SemilatticeSup α] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finsupp.sup_apply {ι : Type u_2} {α : Type u_1} [inst : Zero α] [inst : SemilatticeSup α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} :
↑(f g) i = f i g i
instance Finsupp.lattice {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst : Lattice α] :
Lattice (ι →₀ α)
Equations
  • One or more equations did not get rendered due to their size.

Algebraic order structures #

instance Finsupp.orderedAddCommMonoid {ι : Type u_1} {α : Type u_2} [inst : OrderedAddCommMonoid α] :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
instance Finsupp.contravariantClass {ι : Type u_1} {α : Type u_2} [inst : OrderedAddCommMonoid α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass (ι →₀ α) (ι →₀ α) (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance Finsupp.orderBot {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] :
Equations
theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] :
= 0
@[simp]
theorem Finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] (f : ι →₀ α) (g : ι →₀ α) :
f + g = 0 f = 0 g = 0
theorem Finsupp.le_iff' {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] (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} [inst : CanonicallyOrderedAddMonoid α] (f : ι →₀ α) (g : ι →₀ α) :
f g ∀ (i : ι), i f.supportf i g i
instance Finsupp.decidableLE {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : DecidableRel LE.le] :
Equations
@[simp]
theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] {i : ι} {x : α} {f : ι →₀ α} :
Finsupp.single i x f x f i
instance Finsupp.tsub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : 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_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] :
Equations
  • Finsupp.orderedSub = { tsub_le_iff_right := (_ : ∀ (_n _m _k : ι →₀ α), (∀ (a : ι), ↑(_n - _m) a _k a) ∀ (a : ι), _n a ↑(_k + _m) a) }
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finsupp.coe_tsub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) :
↑(f - g) = f - g
theorem Finsupp.tsub_apply {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) (a : ι) :
↑(f - g) a = f a - g a
@[simp]
theorem Finsupp.single_tsub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] {i : ι} {a : α} {b : α} :
theorem Finsupp.support_tsub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] {f1 : ι →₀ α} {f2 : ι →₀ α} :
(f1 - f2).support f1.support
theorem Finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] [inst : DecidableEq ι] {f1 : ι →₀ α} {f2 : ι →₀ α} :
f1.support \ f2.support (f1 - f2).support
@[simp]
theorem Finsupp.support_inf {ι : Type u_1} {α : Type u_2} [inst : CanonicallyLinearOrderedAddMonoid α] [inst : DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) :
(f g).support = f.support g.support
@[simp]
theorem Finsupp.support_sup {ι : Type u_1} {α : Type u_2} [inst : CanonicallyLinearOrderedAddMonoid α] [inst : DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) :
(f g).support = f.support g.support
theorem Finsupp.disjoint_iff {ι : Type u_1} {α : Type u_2} [inst : CanonicallyLinearOrderedAddMonoid α] {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