essImageDistTriang_mem_of_iso — Mathlib

English

If one triangle T1 is in essImageDistTriang and is isomorphic to T2, then T2 is also in essImageDistTriang.

Русский

Если треугольник T1 принадлежит essImageDistTriang и T2 изоморфен T1, то T2 также принадлежит essImageDistTriang.

LaTeX

$$$(\exists e:\; T_2 \cong T_1),\; T_1 \in L.essImageDistTriang \Rightarrow T_2 \in L.essImageDistTriang$$$

Lean4

theorem essImageDistTriang_mem_of_iso {T₁ T₂ : Triangle D} (e : T₂ ≅ T₁) (h : T₁ ∈ L.essImageDistTriang) :
    T₂ ∈ L.essImageDistTriang := by
  obtain ⟨T', e', hT'⟩ := h
  exact ⟨T', e ≪≫ e', hT'⟩

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