image_ssubset_image_iff — Mathlib

English

If f is injOn on s, then f'' s1 ⊂ f'' s2 iff s1 ⊂ s2, under the same hypotheses as image_subset_image_iff.

Русский

Если f инъективна на s, тогда f '' s1 ⊂ f '' s2 эквивалентно s1 ⊂ s2, при тех же предпосылках, что и image_subset_image_iff.

LaTeX

$$$ \\operatorname{InjOn} f s \\Rightarrow (f '' s_1 \\subset f '' s_2 \\iff s_1 \\subset s_2)$$$

Lean4

theorem image_ssubset_image_iff (h : s.InjOn f) (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂ := by
  simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]
    -- TODO: can this move to a better place?

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