latticeClosure_prod — Mathlib

English

In distributive lattices, the lattice closure of the Cartesian product equals the Cartesian product of the closures: Cl(s × t) = Cl(s) × Cl(t).

Русский

В распределённых решётках замыкание по порядку (lattice closure) произведения равно произведению замыканий: Cl(s × t) = Cl(s) × Cl(t).

LaTeX

$$$\\\\operatorname{latticeClosure}(s \\times t) = \\operatorname{latticeClosure}(s) \\times \\, \\operatorname{latticeClosure}(t)$$$

Lean4

@[simp]
theorem latticeClosure_prod (s : Set α) (t : Set β) : latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t :=
  by simp_rw [← supClosure_infClosure]; simp

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