acuteAngled_reindex_iff — Mathlib

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 [*]

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