# mathlibdocumentation

data.finsupp.lattice

# Lattice structure on finsupps #

This file provides instances of ordered structures on finsupps.

@[protected, instance]
def finsupp.order_bot {α : Type u_1} {μ : Type u_3}  :
Equations
@[protected, instance]
def finsupp.semilattice_inf {α : Type u_1} {β : Type u_2} [has_zero β]  :
Equations
@[simp]
theorem finsupp.inf_apply {α : Type u_1} {β : Type u_2} [has_zero β] {a : α} {f g : α →₀ β} :
(f g) a = f a g a
@[simp]
theorem finsupp.support_inf {α : Type u_1} {γ : Type u_4} {f g : α →₀ γ} :
@[protected, instance]
def finsupp.semilattice_sup {α : Type u_1} {β : Type u_2} [has_zero β]  :
Equations
@[simp]
theorem finsupp.sup_apply {α : Type u_1} {β : Type u_2} [has_zero β] {a : α} {f g : α →₀ β} :
(f g) a = f a g a
@[simp]
theorem finsupp.support_sup {α : Type u_1} {γ : Type u_4} {f g : α →₀ γ} :
@[protected, instance]
def finsupp.lattice {α : Type u_1} {β : Type u_2} [has_zero β] [lattice β] :
lattice →₀ β)
Equations
@[protected, instance]
def finsupp.semilattice_inf_bot {α : Type u_1} {γ : Type u_4}  :
Equations
theorem finsupp.bot_eq_zero {α : Type u_1} {γ : Type u_4}  :
= 0
theorem finsupp.disjoint_iff {α : Type u_1} {γ : Type u_4} {x y : α →₀ γ} :
y
def finsupp.order_embedding_to_fun {α : Type u_1} {β : Type u_2} [has_zero β]  :
→₀ β) ↪o (α → β)

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

Equations
@[simp]
theorem finsupp.order_embedding_to_fun_apply {α : Type u_1} {β : Type u_2} [has_zero β] {f : α →₀ β} {a : α} :
theorem finsupp.monotone_to_fun {α : Type u_1} {β : Type u_2} [has_zero β]  :