English
Rotation of triangles preserves essImageDistTriang membership: T ∈ essImageDistTriang iff T.rotate ∈ essImageDistTriang, under suitable additive and triangulated assumptions on D and L.
Русский
Окружение треугольников сохраняет принадлежность к essImageDistTriang после вращения: T ∈ essImageDistTriang тогда и только тогда, когда T.rotate ∈ essImageDistTriang, при условии аддитивности и триангулированности.
LaTeX
$$$T\in L.essImageDistTriang \iff T^{\text{rotate}} \in L.essImageDistTriang$$$
Lean4
theorem rotate_essImageDistTriang [Preadditive D] [L.Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive]
(T : Triangle D) : T ∈ L.essImageDistTriang ↔ T.rotate ∈ L.essImageDistTriang :=
by
constructor
· rintro ⟨T', e', hT'⟩
exact ⟨T'.rotate, (rotate D).mapIso e' ≪≫ L.mapTriangleRotateIso.app T', rot_of_distTriang T' hT'⟩
· rintro ⟨T', e', hT'⟩
exact
⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫ L.mapTriangleInvRotateIso.app T',
inv_rot_of_distTriang T' hT'⟩
