map_valEmbedding_attachFin — Mathlib

English

Applying the value-embedding map to the attached Finset returns the original finite set.

Русский

Применение отображения значения к прикрепленному Finset возвращает исходное множество.

LaTeX

$$map Fin.valEmbedding (s.attachFin h) = s$$

Lean4

@[simp]
theorem map_valEmbedding_attachFin {s : Finset ℕ} (h : ∀ m ∈ s, m < n) : map Fin.valEmbedding (s.attachFin h) = s := by
  simp [map_eq_image]

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