image_val_attachFin — Mathlib

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⟩

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