module module

`IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalSchedule module_import

declarations in this module (18)

inductive AnalysisAction L24
theorem analysisAction_count L36
def analysisAction L40
theorem analysisAction_injective L51
theorem c3_action L55
theorem c8_action L58
theorem c5_action L61
theorem c9_action L64
theorem c2_action L67
def HasAnalysisAction L71
theorem hasAnalysisAction_all L74
theorem scheduled_has_analysis_action L78
def firstPassActions L84
theorem firstPassActions_eq L87
theorem firstPassActions_length L97
theorem firstPassActions_nodup L102
structure EmpiricalActionPlanCert L107
def empiricalActionPlanCert L125