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 #

source
@[instance_reducible]
instance DFinsupp.instLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] :
LE (Π₀ (i : ι), α i)
source
theorem DFinsupp.le_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] {f g : Π₀ (i : ι), α i} :
f ≤ g ↔ ∀ (i : ι), f i ≤ g i
source
@[simp]
theorem DFinsupp.coe_le_coe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] {f g : Π₀ (i : ι), α i} :
⇑f ≤ ⇑g ↔ f ≤ g
source
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
    source
    @[simp]
    theorem DFinsupp.coe_orderEmbeddingToFun {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] :
    ⇑orderEmbeddingToFun = DFunLike.coe
    source
    theorem DFinsupp.orderEmbeddingToFun_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → LE (α i)] {f : Π₀ (i : ι), α i} {i : ι} :
    orderEmbeddingToFun f i = f i
    source
    @[instance_reducible]
    instance DFinsupp.instPreorder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] :
    Preorder (Π₀ (i : ι), α i)
    source
    theorem DFinsupp.lt_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {f g : Π₀ (i : ι), α i} :
    f < g ↔ f ≤ g ∧ ∃ (i : ι), f i < g i
    source
    @[simp]
    theorem DFinsupp.coe_lt_coe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {f g : Π₀ (i : ι), α i} :
    ⇑f < ⇑g ↔ f < g
    source
    theorem DFinsupp.coe_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] :
    Monotone DFunLike.coe
    source
    theorem DFinsupp.coe_strictMono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] :
    StrictMono DFunLike.coe
    source
    @[simp]
    theorem DFinsupp.single_le_single {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a b : α i} [DecidableEq ι] :
    single i a ≤ single i b ↔ a ≤ b
    source
    theorem DFinsupp.single_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} [DecidableEq ι] :
    Monotone (single i)
    source
    @[simp]
    theorem DFinsupp.single_nonneg {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} [DecidableEq ι] :
    0 ≤ single i a ↔ 0 ≤ a
    source
    @[simp]
    theorem DFinsupp.single_nonpos {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} [DecidableEq ι] :
    single i a ≤ 0 ↔ a ≤ 0
    source
    @[instance_reducible]
    instance DFinsupp.instPartialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] :
    PartialOrder (Π₀ (i : ι), α i)
    source
    @[instance_reducible]
    instance DFinsupp.instSemilatticeInf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] :
    SemilatticeInf (Π₀ (i : ι), α i)
    source
    @[simp]
    theorem DFinsupp.coe_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] (f g : Π₀ (i : ι), α i) :
    ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
    source
    theorem DFinsupp.inf_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
    (f ⊓ g) i = f i ⊓ g i
    source
    @[instance_reducible]
    instance DFinsupp.instSemilatticeSup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] :
    SemilatticeSup (Π₀ (i : ι), α i)
    source
    @[simp]
    theorem DFinsupp.coe_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] (f g : Π₀ (i : ι), α i) :
    ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
    source
    theorem DFinsupp.sup_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
    (f ⊔ g) i = f i ⊔ g i
    source
    @[instance_reducible]
    instance DFinsupp.lattice {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] :
    Lattice (Π₀ (i : ι), α i)
    source
    theorem DFinsupp.support_inf_union_support_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] (f g : Π₀ (i : ι), α i) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] :
    (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
    source
    theorem DFinsupp.support_sup_union_support_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] (f g : Π₀ (i : ι), α i) [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] :
    (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support

    Algebraic order structures #

    source
    instance DFinsupp.instIsOrderedAddMonoid {ι : Type u_1} (α : ι → Type u_3) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)] :
    IsOrderedAddMonoid (Π₀ (i : ι), α i)
    source
    instance DFinsupp.instIsOrderedCancelAddMonoid {ι : Type u_1} (α : ι → Type u_3) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)] :
    IsOrderedCancelAddMonoid (Π₀ (i : ι), α i)
    source
    instance DFinsupp.instAddLeftReflectLE {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), AddLeftReflectLE (α i)] :
    AddLeftReflectLE (Π₀ (i : ι), α i)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    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)
    source
    @[instance_reducible]
    instance DFinsupp.instOrderBotOfIsBotZeroClass {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] :
    OrderBot (Π₀ (i : ι), α i)
    source
    instance DFinsupp.instIsBotZeroClass {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] :
    IsBotZeroClass (Π₀ (i : ι), α i)
    source
    @[deprecated bot_eq_zero (since := "2026-05-07")]
    theorem DFinsupp.bot_eq_zero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] :
    ⊥ = 0
    source
    @[simp]
    theorem DFinsupp.add_eq_zero_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] (f g : Π₀ (i : ι), α i) :
    f + g = 0 ↔ f = 0 ∧ g = 0
    source
    theorem DFinsupp.le_iff' {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f g : Π₀ (i : ι), α i} {s : Finset ι} (hf : f.support ⊆ s) :
    f ≤ g ↔ ∀ i ∈ s, f i ≤ g i
    source
    theorem DFinsupp.le_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f g : Π₀ (i : ι), α i} :
    f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i
    source
    theorem DFinsupp.support_monotone {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] :
    Monotone support
    source
    theorem DFinsupp.support_mono {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] {f g : Π₀ (i : ι), α i} (hfg : f ≤ g) :
    f.support ⊆ g.support
    source
    @[instance_reducible]
    instance DFinsupp.decidableLE {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] [(i : ι) → DecidableLE (α i)] :
    DecidableLE (Π₀ (i : ι), α i)
    source
    @[simp]
    theorem DFinsupp.single_le_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :
    single i a ≤ f ↔ a ≤ f i
    source
    @[instance_reducible]
    instance DFinsupp.tsub {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α 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.

    source
    theorem DFinsupp.tsub_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
    (f - g) i = f i - g i
    source
    @[simp]
    theorem DFinsupp.coe_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] (f g : Π₀ (i : ι), α i) :
    ⇑(f - g) = ⇑f - ⇑g
    source
    instance DFinsupp.instOrderedSub {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] :
    OrderedSub (Π₀ (i : ι), α i)
    source
    instance DFinsupp.instCanonicallyOrderedAddOfAddLeftMono {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] [∀ (i : ι), AddLeftMono (α i)] :
    CanonicallyOrderedAdd (Π₀ (i : ι), α i)
    source
    @[simp]
    theorem DFinsupp.single_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {i : ι} {a b : α i} [DecidableEq ι] :
    single i (a - b) = single i a - single i b
    source
    theorem DFinsupp.support_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {f g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] :
    (f - g).support ⊆ f.support
    source
    theorem DFinsupp.subset_support_tsub {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → Sub (α i)] [∀ (i : ι), OrderedSub (α i)] {f g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] :
    f.support \ g.support ⊆ (f - g).support
    source
    @[simp]
    theorem DFinsupp.support_inf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] [DecidableEq ι] {f g : Π₀ (i : ι), α i} :
    (f ⊓ g).support = f.support ∩ g.support
    source
    @[simp]
    theorem DFinsupp.support_sup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] [DecidableEq ι] {f g : Π₀ (i : ι), α i} :
    (f ⊔ g).support = f.support ∪ g.support
    source
    theorem DFinsupp.disjoint_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsBotZeroClass (α i)] [DecidableEq ι] {f g : Π₀ (i : ι), α i} :
    Disjoint f g ↔ Disjoint f.support g.support