isEquivalence_iff — Mathlib

English

G.IsEquivalence iff G'.IsEquivalence under CatCommSq Φ.functor L1 L2 G.

Русский

G является эквивалентностью тогда и только тогда, когда G' является эквивалентностью под CatCommSq.

LaTeX

$$$G.IsEquivalence \iff G'.IsEquivalence$$$

Lean4

theorem isEquivalence_iff : G.IsEquivalence ↔ G'.IsEquivalence :=
  ⟨fun _ => Φ.isEquivalence_imp L₁ L₂ G L₁' L₂' G', fun _ => Φ.isEquivalence_imp L₁' L₂' G' L₁ L₂ G⟩

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