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

instance Finsupp.instLEFinsupp {ι : Type u_1} {α : Type u_2} [Zero α] [LE α] :

LE (ι →₀ α)

source

theorem Finsupp.le_def {ι : Type u_1} {α : Type u_2} [Zero α] [LE α] {f : ι →₀ α} {g : ι →₀ α} :

f ≤ g ↔ ∀ (i : ι), ↑f i ≤ ↑g i

source

def Finsupp.orderEmbeddingToFun {ι : Type u_1} {α : Type u_2} [Zero α] [LE α] :

(ι →₀ α) ↪o (ι → α)

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

Instances For

source

@[simp]

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

↑Finsupp.orderEmbeddingToFun f i = ↑f i

source

instance Finsupp.preorder {ι : Type u_1} {α : Type u_2} [Zero α] [Preorder α] :

Preorder (ι →₀ α)

source

theorem Finsupp.monotone_toFun {ι : Type u_1} {α : Type u_2} [Zero α] [Preorder α] :

Monotone Finsupp.toFun

source

instance Finsupp.partialorder {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] :

PartialOrder (ι →₀ α)

source

instance Finsupp.semilatticeInf {ι : Type u_1} {α : Type u_2} [Zero α] [SemilatticeInf α] :

SemilatticeInf (ι →₀ α)

source

@[simp]

theorem Finsupp.inf_apply {ι : Type u_1} {α : Type u_2} [Zero α] [SemilatticeInf α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} :

↑(f ⊓ g) i = ↑f i ⊓ ↑g i

source

instance Finsupp.semilatticeSup {ι : Type u_1} {α : Type u_2} [Zero α] [SemilatticeSup α] :

SemilatticeSup (ι →₀ α)

source

@[simp]

theorem Finsupp.sup_apply {ι : Type u_1} {α : Type u_2} [Zero α] [SemilatticeSup α] {i : ι} {f : ι →₀ α} {g : ι →₀ α} :

↑(f ⊔ g) i = ↑f i ⊔ ↑g i

source

instance Finsupp.lattice {ι : Type u_1} {α : Type u_2} [Zero α] [Lattice α] :

Lattice (ι →₀ α)

source

theorem Finsupp.support_inf_union_support_sup {ι : Type u_1} {α : Type u_2} [Zero α] [DecidableEq ι] [Lattice α] (f : ι →₀ α) (g : ι →₀ α) :

(f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support

source

theorem Finsupp.support_sup_union_support_inf {ι : Type u_1} {α : Type u_2} [Zero α] [DecidableEq ι] [Lattice α] (f : ι →₀ α) (g : ι →₀ α) :

(f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support

Algebraic order structures #

source

instance Finsupp.orderedAddCommMonoid {ι : Type u_1} {α : Type u_2} [OrderedAddCommMonoid α] :

OrderedAddCommMonoid (ι →₀ α)

source

instance Finsupp.orderedCancelAddCommMonoid {ι : Type u_1} {α : Type u_2} [OrderedCancelAddCommMonoid α] :

OrderedCancelAddCommMonoid (ι →₀ α)

source

instance Finsupp.contravariantClass {ι : Type u_1} {α : Type u_2} [OrderedAddCommMonoid α] [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

source

instance Finsupp.orderBot {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] :

OrderBot (ι →₀ α)

source

theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] :

⊥ = 0

source

@[simp]

theorem Finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] (f : ι →₀ α) (g : ι →₀ α) :

f + g = 0 ↔ f = 0 ∧ g = 0

source

theorem Finsupp.le_iff' {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] (f : ι →₀ α) (g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) :

f ≤ g ↔ ∀ (i : ι), i ∈ s → ↑f i ≤ ↑g i

source

theorem Finsupp.le_iff {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] (f : ι →₀ α) (g : ι →₀ α) :

f ≤ g ↔ ∀ (i : ι), i ∈ f.support → ↑f i ≤ ↑g i

source

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

DecidableRel LE.le

source

@[simp]

theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] {i : ι} {x : α} {f : ι →₀ α} :

Finsupp.single i x ≤ f ↔ x ≤ ↑f i

source

instance Finsupp.tsub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] :

Sub (ι →₀ α)

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

source

instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] :

OrderedSub (ι →₀ α)

source

instance Finsupp.instCanonicallyOrderedAddMonoidFinsuppToZeroToAddMonoidToAddCommMonoidToOrderedAddCommMonoid {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] :

CanonicallyOrderedAddMonoid (ι →₀ α)

source

@[simp]

theorem Finsupp.coe_tsub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) :

↑(f - g) = ↑f - ↑g

source

theorem Finsupp.tsub_apply {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] (f : ι →₀ α) (g : ι →₀ α) (a : ι) :

↑(f - g) a = ↑f a - ↑g a

source

@[simp]

theorem Finsupp.single_tsub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] {i : ι} {a : α} {b : α} :

Finsupp.single i (a - b) = Finsupp.single i a - Finsupp.single i b

source

theorem Finsupp.support_tsub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] {f1 : ι →₀ α} {f2 : ι →₀ α} :

(f1 - f2).support ⊆ f1.support

source

theorem Finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [Sub α] [OrderedSub α] [DecidableEq ι] {f1 : ι →₀ α} {f2 : ι →₀ α} :

f1.support \ f2.support ⊆ (f1 - f2).support

source

@[simp]

theorem Finsupp.support_inf {ι : Type u_1} {α : Type u_2} [CanonicallyLinearOrderedAddMonoid α] [DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) :

(f ⊓ g).support = f.support ∩ g.support

source

@[simp]

theorem Finsupp.support_sup {ι : Type u_1} {α : Type u_2} [CanonicallyLinearOrderedAddMonoid α] [DecidableEq ι] (f : ι →₀ α) (g : ι →₀ α) :

(f ⊔ g).support = f.support ∪ g.support

source

theorem Finsupp.disjoint_iff {ι : Type u_1} {α : Type u_2} [CanonicallyLinearOrderedAddMonoid α] {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 - Finsupp.single a 1 + u' = u + u' - Finsupp.single a 1

source

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

Pointwise order on finitely supported functions #

Main declarations #

Order structures #

Algebraic order structures #

Some lemmas about ℕ #

Some lemmas about `ℕ` #