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.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

Instances For
    @[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)] :
    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)] :

    Algebraic order structures #

    instance DFinsupp.instOrderedAddCommMonoidDFinsuppToZeroToAddMonoidToAddCommMonoid {ι : Type u_1} (α : ιType u_3) [(i : ι) → OrderedAddCommMonoid (α i)] :
    OrderedAddCommMonoid (Π₀ (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
    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 sf 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 ff 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] :
    @[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.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 ι] :
    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)] :
    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)] :
    @[simp]
    theorem DFinsupp.support_inf {ι : Type u_1} {α : ιType u_2} [(i : ι) → CanonicallyLinearOrderedAddMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} :
    @[simp]
    theorem DFinsupp.support_sup {ι : Type u_1} {α : ιType u_2} [(i : ι) → CanonicallyLinearOrderedAddMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} :
    theorem DFinsupp.disjoint_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → CanonicallyLinearOrderedAddMonoid (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} :