module
module
IndisputableMonolith.Foundation.OptionAEmpiricalSchedule
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (11)
-
def
firstPassSchedule -
theorem
firstPassSchedule_length -
theorem
firstPassSchedule_head -
theorem
firstPassSchedule_second -
theorem
firstPassSchedule_third -
theorem
firstPassSchedule_nodup -
theorem
firstPassSchedule_mem_high_or_immediate -
theorem
firstPassSchedule_mem_iff_high_or_immediate -
theorem
firstPassSchedule_mem_protocol -
structure
EmpiricalScheduleCert -
def
empiricalScheduleCert