English
Projecting the attached Finset back to α via the natural embedding gives back the original Finset: image val of s.attachFin h equals s.
Русский
Проецирование прикрепленного множества обратно через натуральное отображение возвращает исходное множество.
LaTeX
$$image Fin.val (s.attachFin h) = s$$
Lean4
@[simp]
theorem image_val_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) : image Fin.val (s.attachFin h) = s :=
by
apply coe_injective
rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]
exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩