hasse_prod — Mathlib

English

The Hasse diagram of a product order is the box product of the Hasse diagrams.

Русский

Диаграмма Хассе произведения порядков равна коробочной произведению диаграмм Хассе.

LaTeX

$$$hasse (\alpha \times \beta) = hasse \alpha \Box hasse \beta$$$

Lean4

@[simp]
theorem hasse_prod : hasse (α × β) = hasse α □ hasse β :=
  by
  ext x y
  simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm]

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