coeSort_toFinset

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.coeSort_toFinset

← MathLib Explorer

English

There is a type equality between the sort of hs.toFinset and s.

Русский

Имеется равенство типов между типами \$↥hs.toFinset\$ и \$↥s\$.

LaTeX

$$$$ ↥hs.toFinset = ↥s. $$$$

Lean4

/-- Note that this is an equality of types not holding definitionally. Use wisely. -/
theorem coeSort_toFinset : ↥hs.toFinset = ↥s := by rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

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

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

Разделы

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

Аффилиация

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