Documentation

Mathlib.Order.Preorder.Finsupp

Pointwise order on finitely supported functions #

This file lifts order structures on M to ι →₀ M.

source
instance Finsupp.instLE {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] :
LE (ι →₀ M)
Equations
    source
    theorem Finsupp.le_def {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] {f g : ι →₀ M} :
    f ≤ g ↔ ∀ (i : ι), f i ≤ g i
    source
    @[simp]
    theorem Finsupp.coe_le_coe {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] {f g : ι →₀ M} :
    ⇑f ≤ ⇑g ↔ f ≤ g
    source
    def Finsupp.orderEmbeddingToFun {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] :
    (ι →₀ M) ↪o (ι → M)

    The order on Finsupps over a partial order embeds into the order on functions

    Equations
      Instances For
        source
        @[simp]
        theorem Finsupp.orderEmbeddingToFun_apply {ι : Type u_1} {M : Type u_2} [Zero M] [LE M] (f : ι →₀ M) (a : ι) :
        orderEmbeddingToFun f a = f a
        source
        instance Finsupp.preorder {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
        Preorder (ι →₀ M)
        Equations
          source
          theorem Finsupp.lt_def {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] {f g : ι →₀ M} :
          f < g ↔ f ≤ g ∧ ∃ (i : ι), f i < g i
          source
          @[simp]
          theorem Finsupp.coe_lt_coe {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] {f g : ι →₀ M} :
          ⇑f < ⇑g ↔ f < g
          source
          theorem Finsupp.coe_mono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
          Monotone toFun
          source
          theorem Finsupp.coe_strictMono {ι : Type u_1} {M : Type u_2} [Zero M] [Preorder M] :
          Monotone toFun
          source
          instance Finsupp.partialorder {ι : Type u_1} {M : Type u_2} [Zero M] [PartialOrder M] :
          PartialOrder (ι →₀ M)
          Equations
            source
            instance Finsupp.semilatticeInf {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] :
            SemilatticeInf (ι →₀ M)
            Equations
              source
              @[simp]
              theorem Finsupp.inf_apply {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeInf M] (f g : ι →₀ M) (i : ι) :
              (f ⊓ g) i = f i ⊓ g i
              source
              instance Finsupp.semilatticeSup {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] :
              SemilatticeSup (ι →₀ M)
              Equations
                source
                @[simp]
                theorem Finsupp.sup_apply {ι : Type u_1} {M : Type u_2} [Zero M] [SemilatticeSup M] (f g : ι →₀ M) (i : ι) :
                (f ⊔ g) i = f i ⊔ g i
                source
                instance Finsupp.lattice {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] :
                Lattice (ι →₀ M)
                Equations
                  source
                  theorem Finsupp.support_inf_union_support_sup {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] (f g : ι →₀ M) [DecidableEq ι] :
                  (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
                  source
                  theorem Finsupp.support_sup_union_support_inf {ι : Type u_1} {M : Type u_2} [Zero M] [Lattice M] (f g : ι →₀ M) [DecidableEq ι] :
                  (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support