instDecidableLiftOn'OfDecidablePred

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Quotient.instDecidableLiftOn'OfDecidablePred

Lean4

instance (q : Quotient s₁) (f : α → Prop) (h : ∀ a b, s₁ a b → f a = f b) [DecidablePred f] :
    Decidable (Quotient.liftOn' q f h) :=
  Quotient.lift.decidablePred _ _ q

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

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

Разделы

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

Аффилиация

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