subset_map_iff — Mathlib

English

For embeddings f, s ⊆ t.map f iff there exists u ⊆ t with s = u.map f.

Русский

Для вложения f: s ⊆ t.map f эквивалентно существованию u ⊆ t с s = u.map f.

LaTeX

$$$$ s \\subseteq t.map f \\iff \\exists u \\subseteq t, s = u.map f. $$$$

Lean4

theorem subset_map_iff {f : α ↪ β} {s : Finset β} {t : Finset α} : s ⊆ t.map f ↔ ∃ u ⊆ t, s = u.map f := by
  classical simp_rw [map_eq_image, subset_image_iff, eq_comm]

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