preimage_subset_of_subset_image — Mathlib

English

If s is a subset of the image of t under f, then for any injOn f, s.preimage ⊆ t.

Русский

Если s ⊆ f(t), то при любом injOn f, s.preimage ⊆ t.

LaTeX

$$$$ s \\subseteq f[t] \\Rightarrow s.preimage f hf \\subseteq t. $$$$

Lean4

theorem preimage_subset_of_subset_image [DecidableEq β] {f : α → β} {s : Finset β} {t : Finset α} (hs : s ⊆ t.image f)
    {hf} : s.preimage f hf ⊆ t := by rw [← coe_subset, coe_preimage]; exact Set.preimage_subset (mod_cast hs) hf

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