isComplex_iff_of_iso — Mathlib

English

Let e: S1 ≅ S2 be an isomorphism. Then S1.IsComplex ⇔ S2.IsComplex.

Русский

Пусть e: S1 ≅ S2 — изоморфизм. Тогда S1.IsComplex эквивалентно S2.IsComplex.

LaTeX

$$$S_1 \cong S_2 \implies (S_1^{\mathrm{IsComplex}} \iff S_2^{\mathrm{IsComplex}})$$$

Lean4

theorem isComplex_iff_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) : S₁.IsComplex ↔ S₂.IsComplex :=
  ⟨isComplex_of_iso e, isComplex_of_iso e.symm⟩

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