lemma proved term proof

`paramsKernel_verified_any`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  11@[simp] lemma paramsKernel_verified_any (P : Params) (h : ParamProps P) : ParamsKernelVerified P := h

proof body

Term-mode proof.

  12
  13
  14end ILG
  15end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.

ParamProps in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
ParamProps in IndisputableMonolith.ILG.Params decl_use
Params in IndisputableMonolith.ILG.Params decl_use
ParamsKernelVerified in IndisputableMonolith.ILG.ParamsKernel decl_use
ParamProps in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use