LambdaTheoremType

Mathlib.Tactic.FunProp.Theorems

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.LambdaTheoremType

Lean4

/-- Tag for one of the 5 basic lambda theorems -/
inductive LambdaTheoremType/-- Identity theorem e.g. `Continuous fun x => x` -/

  | id/-- Constant theorem e.g. `Continuous fun x => y` -/

  | const/-- Apply theorem e.g. `Continuous fun (f : (x : X) → Y x => f x)` -/

  | apply/-- Composition theorem e.g. `Continuous f → Continuous g → Continuous fun x => f (g x)` -/

  | comp/-- Pi theorem e.g. `∀ y, Continuous (f · y) → Continuous fun x y => f x y` -/

  | pi
  deriving Inhabited, BEq, Repr, Hashable

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

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

Разделы

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

Аффилиация

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