recognition / ILG / ILG.ParamsKernel / ParamsKernelVerified

def

`ParamsKernelVerified`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.ParamsKernel
domain: ILG
line: 8 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.ParamsKernel on GitHub at line 8.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

used by

paramsKernel_verified_any IndisputableMonolith.ILG.ParamsKernel

formal source

   5namespace ILG
   6
   7/-- Verification predicate for the parameter kernel: parameters must be well-formed. -/
   8def ParamsKernelVerified (P : Params) : Prop :=
   9  ParamProps P
  10
  11@[simp] lemma paramsKernel_verified_any (P : Params) (h : ParamProps P) : ParamsKernelVerified P := h
  12
  13
  14end ILG
  15end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.