map_eq_singleton — Mathlib

English

The image map f s is a singleton {b} precisely when s is a singleton {a} and f a = b.

Русский

Образ отображения f на мультимножество s является синглетоном {b} тогда и только тогда, когда s является одиночным множеством {a} и f(a) = b.

LaTeX

$$$$ \\operatorname{map} f s = \\{ b \\} \\iff \\exists a, s = \\{ a \\} \\land f a = b $$$$

Lean4

theorem map_eq_singleton {f : α → β} {s : Multiset α} {b : β} : map f s = { b } ↔ ∃ a : α, s = { a } ∧ f a = b :=
  by
  constructor
  · intro h
    obtain ⟨a, ha⟩ : ∃ a, s = { a } := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
  · rintro ⟨a, rfl, rfl⟩
    simp

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