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

    Equations
      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 DFinsupp.instPreorder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] :
        Preorder (Π₀ (i : ι), α i)
        Equations
          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)] :
          Monotone DFunLike.coe
          source
          instance DFinsupp.instPartialOrder {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] :
          PartialOrder (Π₀ (i : ι), α i)
          Equations
            source
            instance DFinsupp.instSemilatticeInf {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeInf (α i)] :
            SemilatticeInf (Π₀ (i : ι), α i)
            Equations
              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 DFinsupp.instSemilatticeSup {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → SemilatticeSup (α i)] :
              SemilatticeSup (Π₀ (i : ι), α i)
              Equations
                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 DFinsupp.lattice {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → Lattice (α i)] :
                Lattice (Π₀ (i : ι), α i)
                Equations
                  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 DFinsupp.instOrderBot {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] :
                  OrderBot (Π₀ (i : ι), α i)
                  Equations
                    source
                    theorem DFinsupp.bot_eq_zero {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α 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 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)
                    Equations
                      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 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.

                      Equations
                        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 : ι), CanonicallyOrderedAdd (α 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 : ι), CanonicallyOrderedAdd (α 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 : ι), CanonicallyOrderedAdd (α i)] [DecidableEq ι] {f g : Π₀ (i : ι), α i} :
                        Disjoint f g ↔ Disjoint f.support g.support