structure
definition
def or abbrev
Config
show as:
view Lean formalization →
formal statement (Lean)
21structure Config where
22 upsilonStar : ℝ
23 eps_r : ℝ
24 eps_v : ℝ
25 eps_t : ℝ
26 eps_a : ℝ
27
used by (40)
-
default -
additive_emp_left -
additive_emp_right -
additive_strict_of_both_inconsistent -
additive_three -
Calibration -
ConfigSpace -
CostFunction -
cost_ne_zero_of_inconsistent -
cost_pos_iff_inconsistent -
cost_pos_of_inconsistent -
cost_zero_of_consistent -
emp_cost_zero -
extension_to_consistent -
inconsistent_of_join_indep_right -
independent_emp -
join_emp -
recognition_work_constraint_cert -
RecognitionWorkConstraintCert -
recognition_work_constraint_theorem -
uniqueness_on_indep_decomposition -
uniqueness_three_indep -
ConfigProps -
defaultConfig -
gbar_with -
vbarSq_with -
vbar_with -
w_t_nonneg_with -
w_t_ref_with -
w_t_rescale_with