mem_image_iff — Mathlib

English

For x ∈ s, f x ∈ f '' s1 if and only if x ∈ s1, given injOn on s.

Русский

Для x ∈ s, f x ∈ f '' s1 тогда, когда x ∈ s1, при условии инъективности f на s.

LaTeX

$$$ \\forall x, \\operatorname{InjOn} f s \\land (x \\in s) \\Rightarrow (f x \\in f'' s_1 \\iff x \\in s_1)$$$

Lean4

theorem mem_image_iff {x} (hf : InjOn f s) (hs : s₁ ⊆ s) (hx : x ∈ s) : f x ∈ f '' s₁ ↔ x ∈ s₁ :=
  ⟨hf.mem_of_mem_image hs hx, mem_image_of_mem f⟩

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