le_bind — Mathlib

English

If S is a multiset, x ∈ S, then f x ≤ S.bind f (pointwise order).

Русский

Если S — мультимножество, и x ∈ S, то f x ≤ S.bind f (постоянное отношение).

LaTeX

$$$\\forall S\\;\\forall x\\; (x \\in S) \\Rightarrow f x \\le S.bind f$$$

Lean4

theorem le_bind {α β : Type*} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : x ∈ S) : f x ≤ S.bind f := by
  classical
  refine le_iff_count.2 fun a ↦ ?_
  obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
  rw [count_bind, hm', sum_cons]
  exact Nat.le_add_right _ _

Похожие утверждения