isConnected_iff_of_equivalence — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{IsConnected}(K) \\Rightarrow \\text{IsConnected}(J)$ under an equivalence $J \\simeq K$$$

Lean4

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

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