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

ink

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 }

ink

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

ink

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.

ink

@[simp]

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

ink

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

Equations

• Finsupp.preorder = let src := Finsupp.instLEFinsupp; Preorder.mk (_ : ∀ (f : ι →₀ α) (i : ι), ↑f i ≤ ↑f i) (_ : ∀ (f g h : ι →₀ α), f ≤ g → g ≤ h → ∀ (i : ι), ↑f i ≤ ↑h i)

ink

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

ink

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

Equations

• Finsupp.partialorder = let src := Finsupp.preorder; PartialOrder.mk (_ : ∀ (_f _g : ι →₀ α), _f ≤ _g → _g ≤ _f → _f = _g)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[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

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[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

ink

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

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

• @Finsupp.contravariantClass = @Finsupp.contravariantClass.proof_1

ink

instance Finsupp.orderBot {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] : OrderBot (ι →₀ α)

Equations

• Finsupp.orderBot = OrderBot.mk (_ : ∀ (a : ι →₀ α), 0 ≤ a)

ink

theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] : ⊥ = 0

ink

@[simp]

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

ink

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

ink

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

ink

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

Equations

• Finsupp.decidableLE f g = decidable_of_iff (∀ (i : ι), i ∈ f.support → ↑f i ≤ ↑g i) (_ : (∀ (i : ι), i ∈ f.support → ↑f i ≤ ↑g i) ↔ f ≤ g)

ink

@[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

ink

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

• Finsupp.tsub = { sub := Finsupp.zipWith (fun m n => m - n) (_ : 0 - 0 = 0) }

ink

instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] : OrderedSub (ι →₀ α)

Equations

• Finsupp.orderedSub = { tsub_le_iff_right := (_ : ∀ (_n _m _k : ι →₀ α), (∀ (a : ι), ↑(_n - _m) a ≤ ↑_k a) ↔ ∀ (a : ι), ↑_n a ≤ ↑(_k + _m) a) }

ink

instance Finsupp.instCanonicallyOrderedAddMonoidFinsuppToZeroToAddMonoidToAddCommMonoidToOrderedAddCommMonoid {ι : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] : CanonicallyOrderedAddMonoid (ι →₀ α)

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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 ℕ

ink

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

ink

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