theorem
proved
safeBand_contains_phi_point
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Climate.GeoengineeringApproachesFromConfigDim on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
39theorem safeBand_nondegenerate : safeBandLower < safeBandUpper := by
40 unfold safeBandLower safeBandUpper; norm_num
41
42theorem safeBand_contains_phi_point :
43 safeBandLower < 0.118 ∧ 0.118 < safeBandUpper := by
44 unfold safeBandLower safeBandUpper
45 refine ⟨?_, ?_⟩ <;> norm_num
46
47structure GeoengineeringCert where
48 five_approaches : Fintype.card GeoengineeringApproach = 5
49 band_well_defined : safeBandLower < safeBandUpper
50 band_inhabited : safeBandLower < 0.118 ∧ 0.118 < safeBandUpper
51
52noncomputable def geoengineeringCert : GeoengineeringCert where
53 five_approaches := geoengineeringApproach_count
54 band_well_defined := safeBand_nondegenerate
55 band_inhabited := safeBand_contains_phi_point
56
57end IndisputableMonolith.Climate.GeoengineeringApproachesFromConfigDim