image_ssubset_image — Mathlib

English

If s ⊂ t, then s.image f ⊂ t.image f (strict subset preserved under image).

Русский

Если s ⊂ t, то s.image f ⊂ t.image f (строгое включение сохраняется под образованием).

LaTeX

$$$s \subsetneq t \Rightarrow s.image f \subsetneq t.image f$$$

Lean4

theorem image_ssubset_image {t : Finset α} (hf : Injective f) : s.image f ⊂ t.image f ↔ s ⊂ t :=
  by
  simp_rw [← lt_iff_ssubset]
  exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

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