mem_map — Mathlib

English

Membership in the mapped symmetric power corresponds to the existence of a preimage under f.

Русский

Членство в образе отображения Sym соответствует существованию предобраза через f.

LaTeX

$$$\\forall {n} {f} {b} {l},\\ b \\in \\mathrm{Sym.map}(f)(l) \\iff \\exists a,\\ a \\in l \\land f(a)=b.$$$

Lean4

@[simp]
theorem mem_map {n : ℕ} {f : α → β} {b : β} {l : Sym α n} : b ∈ Sym.map f l ↔ ∃ a, a ∈ l ∧ f a = b :=
  Multiset.mem_map

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