English
Let f be an embedding and s a finite set. The collection of n-element subsets of the image s.map f equals the image of the collection of n-element subsets of s under the embedding f.
Русский
Пусть f — вложение, и s — конечное множество. Множество всех подмножеств размера n из образа s.map f равно образу множества всех подмножеств размера n из s под отображением-вложением f.
LaTeX
$$$$\\operatorname{powersetCard}_n(\\operatorname{map} f\\, s) = \\operatorname{map}(\\operatorname{mapEmbedding} f)^{\\toEmbedding}\\bigl(\\operatorname{powersetCard}_n s\\bigr).$$$$
Lean4
theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
ext fun t => by
-- `le_eq_subset` is a dangerous lemma since it turns the type `↪o` into `(· ⊆ ·) ↪r (· ⊆ ·)`,
-- which makes `simp` have trouble working with `mapEmbedding_apply`.
simp only [mem_powersetCard, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply]
constructor
·
classical
intro h
have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
refine ⟨_, ?_, this⟩
rw [← card_map f, this, h.2]; simp
· rintro ⟨a, ⟨has, rfl⟩, rfl⟩
simp only [map_subset_map, has, card_map, and_self]
