fin_map

Mathlib.Data.Finset.Fin

URI: https://scilib.ai/kg/mathlib#Finset.fin_map

← MathLib Explorer

English

(s.fin n).map Fin.valEmbedding = s.filter (\\% < n)

Русский

(s.fin n).map Fin.valEmbedding = s.filter (только меньше n)

LaTeX

$$(s.fin n).map Fin.valEmbedding = s.filter (fun x => x < n)$$

Lean4

@[simp, deprecated map_valEmbedding_attachFin (since := "2025-04-08")]
theorem fin_map {s : Finset ℕ} : (s.fin n).map Fin.valEmbedding = s.filter (· < n) := by
  simp [Finset.fin, Finset.map_map]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru