mem_map_of_injective — Mathlib

English

If f is injective, then for every a and multiset s, f a is in map f s if and only if a is in s.

Русский

Если f инъективна, то для каждого a и мультимножества s верно: f(a) \u2208 map f s тогда и только тогда, когда a \u2208 s.

LaTeX

$$$$ f a \\in \\operatorname{map} f s \\iff a \\in s $$$$

Lean4

@[simp 1100, nolint simpNF]
theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} : f a ∈ map f s ↔ a ∈ s :=
  Quot.inductionOn s fun _l => List.mem_map_of_injective H

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