isConnected_of_equivalent — Mathlib

English

If J and K are equivalent, then if J is connected, K is connected.

Русский

Если J и K эквивалентны и J связно, то и K связано.

LaTeX

$$$\\text{equivalence } e: J \\simeq K \\Rightarrow (\\text{IsConnected}(J) \\Rightarrow \\text{IsConnected}(K))$$$

Lean4

/-- If `J` and `K` are equivalent, then if `J` is connected then `K` is as well. -/
theorem isConnected_of_equivalent {K : Type u₂} [Category.{v₂} K] (e : J ≌ K) [IsConnected J] : IsConnected K :=
  { is_nonempty := Nonempty.map e.functor.obj (by infer_instance)
    toIsPreconnected := isPreconnected_of_equivalent e }

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