mem_map — Mathlib

English

A value b lies in Sym2.map f z iff there exists a with a ∈ z and f a = b.

Русский

Значение b принадлежит Sym2.map f z тогда и только тогда, когда существует a ∈ z такое, что f a = b.

LaTeX

$$$ b \\in Sym2.map f z \\ \\iff\\ \\Exists a,\\ a \\in z \\land f a = b. $$$

Lean4

@[simp]
theorem mem_map {f : α → β} {b : β} {z : Sym2 α} : b ∈ Sym2.map f z ↔ ∃ a, a ∈ z ∧ f a = b :=
  by
  cases z
  simp only [map_pair_eq, mem_iff, exists_eq_or_imp, exists_eq_left]
  aesop

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