image_subset_iff_subset_preimage — Mathlib

English

For an injective f, the condition image s ⊆ t is equivalent to s ⊆ preimage t under f.

Русский

При инъективном f условие image s ⊆ t эквивалентно s ⊆ preimage t относительно f.

LaTeX

$$$$ s \\ image f ⊆ t \\iff s \\subseteq t_{\\mathrm{preimage}} f. $$$$

Lean4

theorem image_subset_iff_subset_preimage [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β}
    (hf : Set.InjOn f (f ⁻¹' ↑t)) : s.image f ⊆ t ↔ s ⊆ t.preimage f hf :=
  image_subset_iff.trans <| by simp only [subset_iff, mem_preimage]

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