decidableEq

Mathlib.Data.Finset.Defs

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

English

Equality on Finset α is decidable whenever α has decidable equality.

Русский

Равенство Finset α разрешимо тогда и только когда α имеет разрешимое равенство.

LaTeX

$$$ [\DecidableEq \alpha] \\Rightarrow \\mathrm{DecidableEq}(\mathrm{Finset} \alpha) $$$

Lean4

instance decidableEq [DecidableEq α] : DecidableEq (Finset α)
  | _, _ => decidable_of_iff _ val_inj

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

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

Разделы

Аффилиация

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