image_eq_image_iff — Mathlib

English

If f is injOn on s, and s1 ⊆ s, s2 ⊆ s, then f'' s1 = f'' s2 iff s1 = s2.

Русский

Если f инъективна на s, и s1 ⊆ s, s2 ⊆ s, тогда f'' s1 = f'' s2 тогда и только тогда, когда s1 = s2.

LaTeX

$$$ \\operatorname{InjOn} f s \\land s_1 \\subseteq s \\land s_2 \\subseteq s \\Rightarrow (f '' s_1 = f '' s_2 \\iff s_1 = s_2)$$$

Lean4

theorem image_eq_image_iff (h : s.InjOn f) (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : f '' s₁ = f '' s₂ ↔ s₁ = s₂ :=
  h.image.eq_iff h₁ h₂

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