delab_set_image_subtype

Mathlib.Data.Set.Notation

URI: https://scilib.ai/kg/mathlib#Set.Notation.delab_set_image_subtype

Lean4

/-- If the `Set.Notation` namespace is open, sets of a subtype coerced to the ambient type are
represented with `↑`.
-/
@[scoped delab app.Set.image]
def delab_set_image_subtype : Delab :=
  whenPPOption getPPCoercions do
    let #[α, _, f, _] := (← getExpr).getAppArgs |
      failure
    guard <| f.isAppOfArity ``Subtype.val 2
    let some _ := α.coeTypeSet? |
      failure
    let e ← withAppArg delab
    `(↑$e)

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

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

Разделы

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

Аффилиация

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