mem_image — Mathlib

English

An element b is in the image of s under f iff there exists a in s with f(a) = b.

Русский

Элемент b принадлежит образу s под f тогда и только тогда, когда существует a ∈ s такое, что f(a) = b.

LaTeX

$$$b \\in \\operatorname{image}(f,s) \\iff \\exists a \\in s, f(a) = b$$$

Lean4

@[simp, grind =]
theorem mem_image : b ∈ s.image f ↔ ∃ a ∈ s, f a = b := by simp only [mem_def, image_val, mem_dedup, Multiset.mem_map]

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