English
Reindexing a simplex by a bijection preserves the property AcuteAngled.
Русский
Переиндексация вершин простого через биекция сохраняет свойство AcuteAngled.
LaTeX
$$$ (s.reindex e).AcuteAngled \iff s.AcuteAngled $$$
Lean4
@[simp]
theorem acuteAngled_reindex_iff {s : Simplex ℝ P m} (e : Fin (m + 1) ≃ Fin (n + 1)) :
(s.reindex e).AcuteAngled ↔ s.AcuteAngled :=
by
refine ⟨fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_, fun h {i₁ i₂ i₃} h₁₂ h₁₃ h₂₃ ↦ ?_⟩
· convert h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1 <;> simp [*]
· convert h (i₁ := e.symm i₁) (i₂ := e.symm i₂) (i₃ := e.symm i₃) ?_ ?_ ?_ using 1 <;> simp [*]