_example

Mathlib.Data.Sum.Interval

URI: https://scilib.ai/kg/mathlib#Sum.Lex._example

Lean4

/-- TODO: `LocallyFiniteOrder.toLocallyFiniteOrderBot` is probably a bad instance, as it forms
a diamond with this instance, and constructs data from data. We should consider removing it. -/
example [Fintype α] [Preorder α] [Preorder β] [OrderBot α] [OrderBot β] [OrderTop α] [LocallyFiniteOrder α]
    [LocallyFiniteOrder β] : LocallyFiniteOrder.toLocallyFiniteOrderBot = instLocallyFiniteOrderBot (α := α) (β := β) :=
  by
  try
    with_reducible_and_instances
      rfl -- fails

  try
    rfl -- fails

  exact Subsingleton.elim _ _

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

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

Разделы

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

Аффилиация

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