image_subset_image_iff — Mathlib

English

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

Русский

Если f инъективна на s, тогда f '' s1 ⊆ f '' s2 эквивалентно s1 ⊆ s2, при условии s1 ⊆ s, s2 ⊆ s.

LaTeX

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

Lean4

theorem image_subset_image_iff (h : s.InjOn f) (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) : f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂ :=
  by
  refine ⟨fun h' ↦ ?_, image_mono⟩
  rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]
  exact inter_subset_inter_left _ (preimage_mono h')

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