LambdaTheoremArgs — Mathlib

Lean4
/-- Tag for one of the 5 basic lambda theorems, that also hold extra data for composition theorem
-/
inductive LambdaTheoremArgs/-- 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)`

  The numbers `fArgId` and `gArgId` store the argument index for `f` and `g` in the composition
  theorem. -/

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

  | pi
  deriving Inhabited, BEq, Repr, Hashable
Похожие утверждения