theorem Finsupp.embDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [PartialOrder α] (f : ι ↪ κ) : Monotone (embDomain f)

theorem Finsupp.embDomain_le_embDomain_iff_le {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [PartialOrder α] (f : ι ↪ κ) (a b : ι →₀ α) : embDomain f a ≤ embDomain f b ↔ a ≤ b

theorem Finsupp.embDomain_lt_embDomain_iff_lt {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [PartialOrder α] (f : ι ↪ κ) (a b : ι →₀ α) : embDomain f a < embDomain f b ↔ a < b

theorem Finsupp.mapDomain_le_mapDomain_iff_le {ι : Type u_4} {κ : Type u_5} {α : Type u_6} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {f : ι → κ} (h : Function.Injective f) (a b : ι →₀ α) : mapDomain f a ≤ mapDomain f b ↔ a ≤ b

theorem Finsupp.mapDomain_lt_mapDomain_iff_lt {ι : Type u_4} {κ : Type u_5} {α : Type u_6} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {f : ι → κ} (h : Function.Injective f) (a b : ι →₀ α) : mapDomain f a < mapDomain f b ↔ a < b