mem_finset_image — Mathlib

English

If f is injective, then b ∈ image f s iff a ∈ s for b = f(a); i.e., membership in the image detects membership in the domain.

Русский

Если f инъективна, то b ∈ image f s эквивалентно существованию a ∈ s с b = f(a); то есть членство в образе определяет членство в области.

LaTeX

$$$\\forall a,\\; f\\text{-инъективность} \\Rightarrow (f(a) \\in \\operatorname{image}(f,s) \\iff a \\in s)$$$

Lean4

theorem _root_.Function.Injective.mem_finset_image (hf : Injective f) : f a ∈ s.image f ↔ a ∈ s :=
  by
  refine ⟨fun h => ?_, Finset.mem_image_of_mem f⟩
  obtain ⟨y, hy, heq⟩ := mem_image.1 h
  exact hf heq ▸ hy

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