coe_fin

Mathlib.Data.Finset.Fin

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

← MathLib Explorer

English

The underlying set of s.fin n equals Fin.val preimage of s’s underlying set.

Русский

Множество, лежащее в основе s.fin n, равно прообразу Fin.val от множества s.

LaTeX

$$(s.fin n).toSet = Set.preimage Fin.val s.toSet$$

Lean4

@[simp, deprecated coe_attachFin (since := "2025-04-08")]
theorem coe_fin (n : ℕ) (s : Finset ℕ) : (s.fin n : Set (Fin n)) = Fin.val ⁻¹' s := by ext; simp

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

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

Разделы

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

Аффилиация

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