Lattice structure on finsupps
This file provides instances of ordered structures on finsupps.
theorem
finsupp.le_def
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[partial_order β]
{a b : α →₀ β} :
@[instance]
Equations
- finsupp.order_bot = {bot := 0, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
def
finsupp.semilattice_inf
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[semilattice_inf β] :
semilattice_inf (α →₀ β)
Equations
- finsupp.semilattice_inf = {inf := finsupp.zip_with has_inf.inf finsupp.semilattice_inf._proof_1, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[simp]
theorem
finsupp.support_inf
{α : Type u_1}
{γ : Type u_4}
[canonically_linear_ordered_add_monoid γ]
{f g : α →₀ γ} :
@[instance]
def
finsupp.semilattice_sup
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[semilattice_sup β] :
semilattice_sup (α →₀ β)
Equations
- finsupp.semilattice_sup = {sup := finsupp.zip_with has_sup.sup finsupp.semilattice_sup._proof_1, le := partial_order.le finsupp.partial_order, lt := partial_order.lt finsupp.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
@[simp]
theorem
finsupp.support_sup
{α : Type u_1}
{γ : Type u_4}
[canonically_linear_ordered_add_monoid γ]
{f g : α →₀ γ} :
@[instance]
Equations
- finsupp.lattice = {sup := semilattice_sup.sup finsupp.semilattice_sup, le := semilattice_inf.le finsupp.semilattice_inf, lt := semilattice_inf.lt finsupp.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf finsupp.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
def
finsupp.semilattice_inf_bot
{α : Type u_1}
{γ : Type u_4}
[canonically_linear_ordered_add_monoid γ] :
semilattice_inf_bot (α →₀ γ)
Equations
- finsupp.semilattice_inf_bot = {bot := order_bot.bot finsupp.order_bot, le := order_bot.le finsupp.order_bot, lt := order_bot.lt finsupp.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := lattice.inf finsupp.lattice, inf_le_left := _, inf_le_right := _, le_inf := _}
theorem
finsupp.bot_eq_zero
{α : Type u_1}
{γ : Type u_4}
[canonically_linear_ordered_add_monoid γ] :
theorem
finsupp.disjoint_iff
{α : Type u_1}
{γ : Type u_4}
[canonically_linear_ordered_add_monoid γ]
{x y : α →₀ γ} :
@[simp]
@[simp]
The order on finsupps over a partial order embeds into the order on functions
Equations
- finsupp.order_embedding_to_fun = {to_embedding := {to_fun := λ (f : α →₀ β) (a : α), ⇑f a, inj' := _}, map_rel_iff' := _}
@[simp]
theorem
finsupp.order_embedding_to_fun_apply
{α : Type u_1}
{β : Type u_2}
[has_zero β]
[partial_order β]
{f : α →₀ β}
{a : α} :
⇑finsupp.order_embedding_to_fun f a = ⇑f a