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.instLEDFinsupp {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] : LE (Π₀ (i : ι), α 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

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

@[simp]

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.instPreorderDFinsupp {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] : Preorder (Π₀ (i : ι), α i)

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

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

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

@[simp]

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.instSemilatticeSupDFinsupp {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] : SemilatticeSup (Π₀ (i : ι), α i)

@[simp]

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)

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)] : DFinsupp.support (f ⊓ g) ∪ DFinsupp.support (f ⊔ g) = DFinsupp.support f ∪ DFinsupp.support g

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)] : DFinsupp.support (f ⊔ g) ∪ DFinsupp.support (f ⊓ g) = DFinsupp.support f ∪ DFinsupp.support g

Algebraic order structures

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

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

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

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

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

@[simp]

theorem DFinsupp.add_eq_zero_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddMonoid (α 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 : ι) → CanonicallyOrderedAddMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} {s : Finset ι} (hf : DFinsupp.support f ⊆ s) : f ≤ g ↔ ∀ (i : ι), i ∈ s → ↑f i ≤ ↑g i

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

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

@[simp]

theorem DFinsupp.single_le_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddMonoid (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} : DFinsupp.single i a ≤ f ↔ a ≤ ↑f i

instance DFinsupp.tsub {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CanonicallyOrderedAddMonoid (α 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.

theorem DFinsupp.tsub_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddMonoid (α 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 : ι) → CanonicallyOrderedAddMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) : ↑(f - g) = ↑f - ↑g

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

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

@[simp]

theorem DFinsupp.single_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddMonoid (α 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 : ι) → CanonicallyOrderedAddMonoid (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] : DFinsupp.support (f - g) ⊆ DFinsupp.support f

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

@[simp]

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

@[simp]

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

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