termTo_app_of%_

Mathlib.Tactic.CategoryTheory.ToApp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.termTo_app_of%_

Lean4

/-- Given an equation `t` of the form `η = θ` between 2-morphisms `f ⟶ g` with `f g : C ⟶ D` in the
bicategory `Cat` (possibly after a `∀` binder), `to_app_of% t` produces the equation
`∀ (X : C), η.app X = θ.app X` (where `X` is an object in the domain of `f` and `g`), and simplifies
it suitably using basic lemmas about `NatTrans.app`.
-/
@[term_parser 1000]
public meta def «termTo_app_of%_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `CategoryTheory.«termTo_app_of%_» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "to_app_of% ") (ParserDescr.cat✝ `term 0))

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

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

Разделы

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

Аффилиация

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