prod_top — Mathlib

English

For a Sublattice L of α, the product with the top Sublattice of β equals the comap of fst: L.prod ⊤ = L.comap fst.

Русский

Для подпредела L в α произведение с верхом β даёт то же, что и обратное отображение fst: L.prod ⊤ = L.comap fst.

LaTeX

$$$L \\ prod (\\top) = L \\ comap (fst)$$$

Lean4

theorem prod_top (L : Sublattice α) : L.prod (⊤ : Sublattice β) = L.comap LatticeHom.fst :=
  ext fun a ↦ by simp [mem_prod, LatticeHom.coe_fst]

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