map_subset_iff_subset_preimage — Mathlib

English

For an embedding f, s.map f ⊆ t is equivalent to s ⊆ t.preimage f.

Русский

Для вложения f, s.map f ⊆ t эквивалентно s ⊆ t.preimage f.

LaTeX

$$$$ s\\mapsto f \\subseteq t \\iff s \\subseteq t.preimage f f.injective.injOn. $$$$

Lean4

theorem map_subset_iff_subset_preimage {f : α ↪ β} {s : Finset α} {t : Finset β} :
    s.map f ⊆ t ↔ s ⊆ t.preimage f f.injective.injOn := by classical rw [map_eq_image, image_subset_iff_subset_preimage]

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