acuteAngled

Mathlib.Geometry.Euclidean.Simplex

URI: https://scilib.ai/kg/mathlib#Affine.Simplex.Equilateral.acuteAngled

← MathLib Explorer

English

If a simplex is equilateral, then every angle is acute.

Русский

Если простойм равносторонний, то каждый угол острый.

LaTeX

$$$s.Equilateral \Rightarrow s.AcuteAngled$$$

Lean4

theorem acuteAngled {s : Simplex ℝ P n} (he : s.Equilateral) : s.AcuteAngled :=
  by
  intro i₁ i₂ i₃ h₁₂ h₁₃ h₂₃
  rw [he.angle_eq_pi_div_three h₁₂ h₁₃ h₂₃]
  linarith [Real.pi_pos]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru