ofBoxProdLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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