map_subset_map — Mathlib

English

For Finsets s1, s2 and embedding f, s1.map f ⊆ s2.map f iff s1 ⊆ s2.

Русский

Пусть s1, s2 — Finset, и f — вложение; тогда s1.map f ⊆ s2.map f тогда и только тогда s1 ⊆ s2.

LaTeX

$$$s_1.map f \subseteq s_2.map f \iff s_1 \subseteq s_2$$$

Lean4

@[simp]
theorem map_subset_map {s₁ s₂ : Finset α} : s₁.map f ⊆ s₂.map f ↔ s₁ ⊆ s₂ :=
  ⟨fun h _ xs => (mem_map' _).1 <| h <| (mem_map' f).2 xs, fun h => by simp [subset_def, Multiset.map_subset_map h]⟩

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