mem_map — Mathlib

English

For a function f : α → β and a multiset s of α, b ∈ map f s iff there exists a ∈ s with f a = b.

Русский

Для отображения f: α→β и мультимножества s, b ∈ map f s эквивалентно существованию a ∈ s с f a = b.

LaTeX

$$$$ b \\in \\mathrm{map} f s \\iff \\exists a, a \\in s \\wedge f a = b $$$$

Lean4

@[simp]
theorem mem_map {f : α → β} {b : β} {s : Multiset α} : b ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b :=
  Quot.inductionOn s fun _l => List.mem_map

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