map_eq_zero — Mathlib

English

For any multiset s and function f, map f s equals the empty multiset if and only if s is the empty multiset.

Русский

Для любого мультимножества s и функции f отображение map f s равно пустому мультимножеству тогда и только тогда, когда само s пусто.

LaTeX

$$$$ \\operatorname{map} f s = 0 \\iff s = 0 $$$$

Lean4

@[simp]
theorem map_eq_zero {s : Multiset α} {f : α → β} : s.map f = 0 ↔ s = 0 := by
  rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]

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