ofBoxProdRight — Mathlib

English

If the box product G □ H is preconnected and H is nonempty, then H is preconnected.

Русский

Если box-продукт G □ H предсвязен и H непуст, то H предсвязан.

LaTeX

$$[Nonempty α] (G □ H).Preconnected → H.Preconnected$$

Lean4

protected theorem ofBoxProdRight [Nonempty α] (h : (G □ H).Preconnected) : H.Preconnected := by
  classical
  rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩

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