Pointwise order on finitely supported dependent functions

This file lifts order structures on the α i to Π₀ i, α i.

Main declarations

• DFinsupp.orderEmbeddingToFun: The order embedding from finitely supported dependent functions to functions.

Order structures

instance DFinsupp.instLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] : LE (Π₀ (i : ι), α i)

Equations

• DFinsupp.instLE = { le := fun (f g : Π₀ (i : ι), α i) => ∀ (i : ι), f i ≤ g i }

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

@[simp]

theorem DFinsupp.coe_le_coe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : ⇑f ≤ ⇑g ↔ f ≤ g

def DFinsupp.orderEmbeddingToFun {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] : (Π₀ (i : ι), α i) ↪o ((i : ι) → α i)

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

Equations

• DFinsupp.orderEmbeddingToFun = { toFun := DFunLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem DFinsupp.coe_orderEmbeddingToFun {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] : ⇑DFinsupp.orderEmbeddingToFun = DFunLike.coe

theorem DFinsupp.orderEmbeddingToFun_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] {f : Π₀ (i : ι), α i} {i : ι} : DFinsupp.orderEmbeddingToFun f i = f i

instance DFinsupp.instPreorder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] : Preorder (Π₀ (i : ι), α i)

Equations

• DFinsupp.instPreorder = Preorder.mk ⋯ ⋯ ⋯

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

@[simp]

theorem DFinsupp.coe_lt_coe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : ⇑f < ⇑g ↔ f < g

theorem DFinsupp.coe_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] : Monotone DFunLike.coe

theorem DFinsupp.coe_strictMono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] : Monotone DFunLike.coe

instance DFinsupp.instPartialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] : PartialOrder (Π₀ (i : ι), α i)

Equations

• DFinsupp.instPartialOrder = PartialOrder.mk ⋯

instance DFinsupp.instSemilatticeInf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] : SemilatticeInf (Π₀ (i : ι), α i)

Equations

• DFinsupp.instSemilatticeInf = SemilatticeInf.mk ⋯ ⋯ ⋯

@[simp]

theorem DFinsupp.coe_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) : ⇑(f ⊓ g) = ⇑f ⊓ ⇑g

theorem DFinsupp.inf_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) (i : ι) : (f ⊓ g) i = f i ⊓ g i

instance DFinsupp.instSemilatticeSup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] : SemilatticeSup (Π₀ (i : ι), α i)

Equations

• DFinsupp.instSemilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯

@[simp]

theorem DFinsupp.coe_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) : ⇑(f ⊔ g) = ⇑f ⊔ ⇑g

theorem DFinsupp.sup_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) (i : ι) : (f ⊔ g) i = f i ⊔ g i

instance DFinsupp.lattice {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] : Lattice (Π₀ (i : ι), α i)

Equations

• DFinsupp.lattice = Lattice.mk ⋯ ⋯ ⋯

theorem DFinsupp.support_inf_union_support_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support

theorem DFinsupp.support_sup_union_support_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support

Algebraic order structures

instance DFinsupp.instOrderedAddCommMonoid {ι : Type u_1} (α : ι → Type u_3) [(i : ι) → OrderedAddCommMonoid (α i)] : OrderedAddCommMonoid (Π₀ (i : ι), α i)

Equations

• DFinsupp.instOrderedAddCommMonoid α = OrderedAddCommMonoid.mk ⋯

instance DFinsupp.instOrderedCancelAddCommMonoid {ι : Type u_1} (α : ι → Type u_3) [(i : ι) → OrderedCancelAddCommMonoid (α i)] : OrderedCancelAddCommMonoid (Π₀ (i : ι), α i)

Equations

• DFinsupp.instOrderedCancelAddCommMonoid α = OrderedCancelAddCommMonoid.mk ⋯

instance DFinsupp.instContravariantClassHAddLe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → OrderedAddCommMonoid (α i)] [∀ (i : ι), ContravariantClass (α i) (α i) (fun (x1 x2 : α i) => x1 + x2) fun (x1 x2 : α i) => x1 ≤ x2] : ContravariantClass (Π₀ (i : ι), α i) (Π₀ (i : ι), α i) (fun (x1 x2 : Π₀ (i : ι), α i) => x1 + x2) fun (x1 x2 : Π₀ (i : ι), α i) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance DFinsupp.instPosSMulMono {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [Preorder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Preorder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), PosSMulMono α (β i)] : PosSMulMono α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instSMulPosMono {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [Preorder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Preorder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), SMulPosMono α (β i)] : SMulPosMono α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instPosSMulReflectLE {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [Preorder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Preorder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), PosSMulReflectLE α (β i)] : PosSMulReflectLE α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instSMulPosReflectLE {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [Preorder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Preorder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), SMulPosReflectLE α (β i)] : SMulPosReflectLE α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instPosSMulStrictMono {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [PartialOrder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → PartialOrder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), PosSMulStrictMono α (β i)] : PosSMulStrictMono α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instSMulPosStrictMono {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [PartialOrder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → PartialOrder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), SMulPosStrictMono α (β i)] : SMulPosStrictMono α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instSMulPosReflectLT {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [Semiring α] [PartialOrder α] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → PartialOrder (β i)] [(i : ι) → Module α (β i)] [∀ (i : ι), SMulPosReflectLT α (β i)] : SMulPosReflectLT α (Π₀ (i : ι), β i)

Equations

• ⋯ = ⋯

instance DFinsupp.instOrderBot {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] : OrderBot (Π₀ (i : ι), α i)

Equations

• DFinsupp.instOrderBot α = OrderBot.mk ⋯

theorem DFinsupp.bot_eq_zero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] : ⊥ = 0

@[simp]

theorem DFinsupp.add_eq_zero_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) : f + g = 0 ↔ f = 0 ∧ g = 0

theorem DFinsupp.le_iff' {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} {s : Finset ι} (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

theorem DFinsupp.le_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i

theorem DFinsupp.support_monotone {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : Monotone DFinsupp.support

theorem DFinsupp.support_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} (hfg : f ≤ g) : f.support ⊆ g.support

instance DFinsupp.decidableLE {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] [(i : ι) → DecidableRel LE.le] : DecidableRel LE.le

Equations

• DFinsupp.decidableLE α x✝ x = decidable_of_iff (∀ i ∈ x✝.support, x✝ i ≤ x i) ⋯

@[simp]

theorem DFinsupp.single_le_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} : DFinsupp.single i a ≤ f ↔ a ≤ f i

instance DFinsupp.tsub {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] : Sub (Π₀ (i : ι), α i)

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

Equations

• DFinsupp.tsub α = { sub := DFinsupp.zipWith (fun (x : ι) (m n : α x) => m - n) ⋯ }

theorem DFinsupp.tsub_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) (i : ι) : (f - g) i = f i - g i

@[simp]

theorem DFinsupp.coe_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) : ⇑(f - g) = ⇑f - ⇑g

instance DFinsupp.instOrderedSub {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] : OrderedSub (Π₀ (i : ι), α i)

Equations

• ⋯ = ⋯

instance DFinsupp.instCanonicallyOrderedAddCommMonoid {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] : CanonicallyOrderedAddCommMonoid (Π₀ (i : ι), α i)

Equations

• DFinsupp.instCanonicallyOrderedAddCommMonoid α = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

@[simp]

theorem DFinsupp.single_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {i : ι} {a : α i} {b : α i} [DecidableEq ι] : DFinsupp.single i (a - b) = DFinsupp.single i a - DFinsupp.single i b

theorem DFinsupp.support_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : (f - g).support ⊆ f.support

theorem DFinsupp.subset_support_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : f.support \ g.support ⊆ (f - g).support

@[simp]

theorem DFinsupp.support_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : (f ⊓ g).support = f.support ∩ g.support

@[simp]

theorem DFinsupp.support_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : (f ⊔ g).support = f.support ∪ g.support

theorem DFinsupp.disjoint_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} : Disjoint f g ↔ Disjoint f.support g.support