isConnected_iff_of_initial — Mathlib

English

The domain of an initial functor is connected if the functor has an initial object; more generally, when F.Initial holds, IsConnected C ⇔ IsConnected D.

Русский

Область определения инициального функторa связана, если существует начальный объект; в общем случае IsConnected C ⇔ IsConnected D при [F.Initial].

LaTeX

$$$\IsConnected C \iff \IsConnected D$ \quad \text{given } F: C \to D \text{ with } F.Initial$$$

Lean4

/-- The domain of an initial functor is connected if and only if its codomain is connected. -/
theorem isConnected_iff_of_initial (F : C ⥤ D) [F.Initial] : IsConnected C ↔ IsConnected D :=
  by
  rw [← isConnected_op_iff_isConnected C, ← isConnected_op_iff_isConnected D]
  exact isConnected_iff_of_final F.op

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