instDecidableInjOnToSetOfDecidableEq

Mathlib.Data.Fintype.Defs

URI: https://scilib.ai/kg/mathlib#List.instDecidableInjOnToSetOfDecidableEq

Lean4

instance [DecidableEq β] : Decidable (Set.InjOn f s) :=
  -- Use custom implementation for better performance.

  decidable_of_iff ((Multiset.map f s.val).Nodup) Finset.nodup_map_iff_injOn

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

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

Разделы

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

Аффилиация

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