isConnected_comma_of_initial — Mathlib

English

Let A be connected and R final; then Comma L R is connected.

Русский

Пусть A связана, а R финальная; тогда Comma L R связана.

LaTeX

$$$\\\\operatorname{IsConnected}(\\\\operatorname{Comma}(L,R))$$$

Lean4

/-- `Comma L R` with `L : A ⥤ T` and `R : B ⥤ T` is connected if `L` is initial and `B` is
connected. -/
instance isConnected_comma_of_initial [IsConnected B] [L.Initial] : IsConnected (Comma L R) := by
  rwa [isConnected_iff_of_initial (snd L R)]

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