coe_image — Mathlib

English

The coercion of the image Finset to a Set equals the Set image of s to the image of f: ↑(image f s) = f '' ↑s.

Русский

Приведение образа Finset к множеству равно образу множества через f: ↑(image f s) = f '' ↑s.

LaTeX

$$$\\uparrow (\\operatorname{image}(f,s)) = f''\\uparrow s$$$

Lean4

@[simp, norm_cast]
theorem coe_image : ↑(s.image f) = f '' ↑s :=
  Set.ext <| by simp only [mem_coe, mem_image, Set.mem_image, implies_true]

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