toFinset_congr

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Set.toFinset_congr

English

If two sets are equal, their finite enumerations are equal as Finsets.

Русский

Если два множества равны, их конечные перечисления равны как Finset-элементы.

LaTeX

$$$s = t \Rightarrow s.toFinset = t.toFinset$$$

Lean4

@[congr]
theorem toFinset_congr {s t : Set α} [Fintype s] [Fintype t] (h : s = t) : toFinset s = toFinset t := by subst h; congr!

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

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

Разделы

Аффилиация

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