Pointwise order on finitely supported functions #
This file lifts order structures on α to ι →₀ α.
Main declarations #
finsupp.order_embedding_to_fun: The order embedding from finitely supported functions to functions.finsupp.order_iso_multiset: The order isomorphism betweenℕ-valued finitely supported functions and multisets.
Order structures #
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 : ι →₀ α), ⇑f, inj' := _}, map_rel_iff' := _}
@[simp]
theorem
finsupp.order_embedding_to_fun_apply
{ι : Type u_1}
{α : Type u_2}
[has_zero α]
[has_le α]
{f : ι →₀ α}
{i : ι} :
⇑finsupp.order_embedding_to_fun f i = ⇑f i
@[protected, instance]
def
finsupp.partial_order
{ι : Type u_1}
{α : Type u_2}
[has_zero α]
[partial_order α] :
partial_order (ι →₀ α)
Equations
- finsupp.partial_order = {le := preorder.le finsupp.preorder, lt := preorder.lt finsupp.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
noncomputable
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 := _}
@[protected, instance]
noncomputable
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 := _}
@[protected, 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 := _}
Algebraic order structures #
@[protected, instance]
noncomputable
def
finsupp.ordered_add_comm_monoid
{ι : Type u_1}
{α : Type u_2}
[ordered_add_comm_monoid α] :
ordered_add_comm_monoid (ι →₀ α)
Equations
- finsupp.ordered_add_comm_monoid = {add := add_comm_monoid.add finsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero finsupp.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul finsupp.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, 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 := _, add_le_add_left := _}
@[protected, instance]
noncomputable
def
finsupp.ordered_cancel_add_comm_monoid
{ι : Type u_1}
{α : Type u_2}
[ordered_cancel_add_comm_monoid α] :
Equations
- finsupp.ordered_cancel_add_comm_monoid = {add := ordered_add_comm_monoid.add finsupp.ordered_add_comm_monoid, add_assoc := _, add_left_cancel := _, zero := ordered_add_comm_monoid.zero finsupp.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul finsupp.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le finsupp.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt finsupp.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}
@[protected, instance]
def
finsupp.has_le.le.contravariant_class
{ι : Type u_1}
{α : Type u_2}
[ordered_add_comm_monoid α]
[contravariant_class α α has_add.add has_le.le] :
contravariant_class (ι →₀ α) (ι →₀ α) has_add.add has_le.le
@[protected, instance]
Equations
- finsupp.order_bot = {bot := 0, bot_le := _}
@[protected]
@[simp]
theorem
finsupp.add_eq_zero_iff
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
(f g : ι →₀ α) :
@[protected, instance]
def
finsupp.decidable_le
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[decidable_rel has_le.le] :
Equations
- finsupp.decidable_le = λ (f g : ι →₀ α), decidable_of_iff (∀ (i : ι), i ∈ f.support → ⇑f i ≤ ⇑g i) _
@[simp]
theorem
finsupp.single_le_iff
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
{i : ι}
{x : α}
{f : ι →₀ α} :
finsupp.single i x ≤ f ↔ x ≤ ⇑f i
@[protected, instance]
noncomputable
def
finsupp.tsub
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α] :
This is called tsub for truncated subtraction, to distinguish it with subtraction in an
additive group.
Equations
- finsupp.tsub = {sub := finsupp.zip_with (λ (m n : α), m - n) finsupp.tsub._proof_1}
@[protected, instance]
def
finsupp.has_ordered_sub
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α] :
has_ordered_sub (ι →₀ α)
Equations
@[protected, instance]
noncomputable
def
finsupp.canonically_ordered_add_monoid
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α] :
Equations
- finsupp.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add finsupp.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero finsupp.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul finsupp.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_add_comm_monoid.le finsupp.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt finsupp.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot finsupp.order_bot, bot_le := _, le_iff_exists_add := _}
@[simp]
theorem
finsupp.coe_tsub
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(f g : ι →₀ α) :
theorem
finsupp.tsub_apply
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(f g : ι →₀ α)
(a : ι) :
@[simp]
theorem
finsupp.single_tsub
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{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}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{f1 f2 : ι →₀ α} :
theorem
finsupp.subset_support_tsub
{ι : Type u_1}
{α : Type u_2}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{f1 f2 : ι →₀ α} :
@[simp]
theorem
finsupp.support_inf
{ι : Type u_1}
{α : Type u_2}
[canonically_linear_ordered_add_monoid α]
[decidable_eq ι]
{f g : ι →₀ α} :
@[simp]
theorem
finsupp.support_sup
{ι : Type u_1}
{α : Type u_2}
[canonically_linear_ordered_add_monoid α]
[decidable_eq ι]
{f g : ι →₀ α} :
theorem
finsupp.disjoint_iff
{ι : Type u_1}
{α : Type u_2}
[canonically_linear_ordered_add_monoid α]
[decidable_eq ι]
{f g : ι →₀ α} :
Some lemmas about ℕ #
theorem
finsupp.sub_single_one_add
{ι : Type u_1}
{a : ι}
{u u' : ι →₀ ℕ}
(h : ⇑u a ≠ 0) :
u - finsupp.single a 1 + u' = u + u' - finsupp.single a 1
theorem
finsupp.add_sub_single_one
{ι : Type u_1}
{a : ι}
{u u' : ι →₀ ℕ}
(h : ⇑u' a ≠ 0) :
u + (u' - finsupp.single a 1) = u + u' - finsupp.single a 1