Documentation

Mathlib.Data.DFinsupp.Order

Pointwise order on finitely supported dependent functions #

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

Main declarations #

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
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
instance DFinsupp.instSemilatticeInf {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] :
SemilatticeInf (Π₀ (i : ι), α i)
Equations
@[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
@[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
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
instance DFinsupp.instAddLeftReflectLE {ι : Type u_1} {α : ιType u_2} [(i : ι) → OrderedAddCommMonoid (α i)] [∀ (i : ι), AddLeftReflectLE (α i)] :
AddLeftReflectLE (Π₀ (i : ι), α i)
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
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 is, 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 if.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] :
Equations
@[simp]
theorem DFinsupp.single_le_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {i : ι} {a : α 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
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
@[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 ι] :
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