English
The Cartesian product of two incidence algebras is itself an incidence algebra on the product preorder, with the product defined pointwise: (f.prod g)((x1,y1),(x2,y2)) = f(x1,y1) · g(x2,y2).
Русский
Декартово произведение двух инцидентных алгебр снова образует инцидентную алгебру над порядком α × β, причем произведение задается покомпонентно: (f.prod g)((x1,y1),(x2,y2)) = f(x1,y1) · g(x2,y2).
LaTeX
$$$ (f \mathrm{prod}\ g)((a_1,b_1),(a_2,b_2)) = f(a_1,a_2) \cdot g(b_1,b_2) $$$
Lean4
/-- The Cartesian product of two incidence algebras. -/
protected def prod : IncidenceAlgebra 𝕜 (α × β)
where
toFun x y := f x.1 y.1 * g x.2 y.2
eq_zero_of_not_le' x y
hxy := by
rw [Prod.le_def, not_and_or] at hxy
obtain hxy | hxy := hxy <;> simp [apply_eq_zero_of_not_le hxy]
