Pointwise order on finitely supported functions #
This file lifts order structures on α
to ι →₀ α→₀ α
.
Main declarations #
Finsupp.orderEmbeddingToFun
: The order embedding from finitely supported functions to functions.
Order structures #
instance
Finsupp.partialorder
{ι : Type u_1}
{α : Type u_2}
[inst : Zero α]
[inst : PartialOrder α]
:
PartialOrder (ι →₀ α)
instance
Finsupp.semilatticeInf
{ι : Type u_1}
{α : Type u_2}
[inst : Zero α]
[inst : SemilatticeInf α]
:
SemilatticeInf (ι →₀ α)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.semilatticeSup
{ι : Type u_1}
{α : Type u_2}
[inst : Zero α]
[inst : SemilatticeSup α]
:
SemilatticeSup (ι →₀ α)
Equations
- One or more equations did not get rendered due to their size.
Algebraic order structures #
instance
Finsupp.orderedAddCommMonoid
{ι : Type u_1}
{α : Type u_2}
[inst : OrderedAddCommMonoid α]
:
OrderedAddCommMonoid (ι →₀ α)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.orderedCancelAddCommMonoid
{ι : Type u_1}
{α : Type u_2}
[inst : OrderedCancelAddCommMonoid α]
:
OrderedCancelAddCommMonoid (ι →₀ α)
Equations
- One or more equations did not get rendered due to their size.
instance
Finsupp.contravariantClass
{ι : Type u_1}
{α : Type u_2}
[inst : OrderedAddCommMonoid α]
[inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
ContravariantClass (ι →₀ α) (ι →₀ α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
Equations
- Finsupp.orderBot = OrderBot.mk (_ : ∀ (a : ι →₀ α), 0 ≤ a)
instance
Finsupp.decidableLE
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : DecidableRel LE.le]
:
DecidableRel LE.le
Equations
- Finsupp.decidableLE f g = decidable_of_iff (∀ (i : ι), i ∈ f.support → ↑f i ≤ ↑g i) (_ : (∀ (i : ι), i ∈ f.support → ↑f i ≤ ↑g i) ↔ f ≤ g)
@[simp]
theorem
Finsupp.single_le_iff
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
{i : ι}
{x : α}
{f : ι →₀ α}
:
Finsupp.single i x ≤ f ↔ x ≤ ↑f i
instance
Finsupp.tsub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
:
This is called tsub
for truncated subtraction, to distinguish it with subtraction in an
additive group.
Equations
- Finsupp.tsub = { sub := Finsupp.zipWith (fun m n => m - n) (_ : 0 - 0 = 0) }
instance
Finsupp.orderedSub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
:
OrderedSub (ι →₀ α)
instance
Finsupp.instCanonicallyOrderedAddMonoidFinsuppToZeroToAddMonoidToAddCommMonoidToOrderedAddCommMonoid
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Finsupp.coe_tsub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
(f : ι →₀ α)
(g : ι →₀ α)
:
theorem
Finsupp.tsub_apply
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
(f : ι →₀ α)
(g : ι →₀ α)
(a : ι)
:
@[simp]
theorem
Finsupp.single_tsub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
{i : ι}
{a : α}
{b : α}
:
Finsupp.single i (a - b) = Finsupp.single i a - Finsupp.single i b
theorem
Finsupp.support_tsub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
{f1 : ι →₀ α}
{f2 : ι →₀ α}
:
theorem
Finsupp.subset_support_tsub
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
[inst : DecidableEq ι]
{f1 : ι →₀ α}
{f2 : ι →₀ α}
:
@[simp]
theorem
Finsupp.support_inf
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyLinearOrderedAddMonoid α]
[inst : DecidableEq ι]
(f : ι →₀ α)
(g : ι →₀ α)
:
@[simp]
theorem
Finsupp.support_sup
{ι : Type u_1}
{α : Type u_2}
[inst : CanonicallyLinearOrderedAddMonoid α]
[inst : DecidableEq ι]
(f : ι →₀ α)
(g : ι →₀ α)
: