isPreconnected_iff_of_equivalence

English

An equivalence of categories preserves preconnectedness in both directions.

Русский

Эквивалентность категорий сохраняет предсвязность в обе стороны.

LaTeX

$$$\\text{IsPreconnected}(J) \\iff \\text{IsPreconnected}(K)$ for an equivalence $J \\simeq K$.$$

Lean4

theorem isPreconnected_iff_of_equivalence {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) :
    IsPreconnected J ↔ IsPreconnected K :=
  ⟨fun _ => isPreconnected_of_equivalent e, fun _ => isPreconnected_of_equivalent e.symm⟩

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