top_prod

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.top_prod

English

For a Sublattice L of α, (⊤) .prod L equals L.comap fst.

Русский

Для подпредела L в α, (⊤) .prod L = L.comap fst.

LaTeX

$$LeftTop := (\\top).prod L = L.comap (fst)$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru