theorem
proved
cos_theta
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Geometry.DihedralAngle on GitHub at line 72.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
69 Real.arccos_le_pi d.cosine
70
71/-- `cos θ = cosine` by construction. -/
72theorem cos_theta (d : DihedralAngleData) : Real.cos d.theta = d.cosine := by
73 unfold DihedralAngleData.theta
74 exact Real.cos_arccos d.cosine_lb d.cosine_ub
75
76/-! ## §2. Canonical values -/
77
78/-- A regular tetrahedron's dihedral angle has cosine `1/3`. -/
79def regular_tet_dihedral : DihedralAngleData :=
80 { cosine := 1 / 3
81 , cosine_lb := by norm_num
82 , cosine_ub := by norm_num
83 }
84
85/-- The regular-tetrahedron dihedral angle is `arccos(1/3) ≈ 70.53°`. -/
86theorem regular_tet_dihedral_theta :
87 regular_tet_dihedral.theta = Real.arccos (1/3) := rfl
88
89/-- `arccos(1/3)` lies strictly between 0 and π. -/
90theorem regular_tet_dihedral_in_open_interval :
91 0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi := by
92 refine ⟨?_, ?_⟩
93 · rw [regular_tet_dihedral_theta]
94 apply Real.arccos_pos.mpr
95 norm_num
96 · rw [regular_tet_dihedral_theta]
97 have h_le : Real.arccos (1/3) ≤ Real.pi := Real.arccos_le_pi _
98 have h_ne : Real.arccos (1/3) ≠ Real.pi := by
99 intro h_eq
100 rw [Real.arccos_eq_pi] at h_eq
101 linarith
102 exact lt_of_le_of_ne h_le h_ne