bot_prod

Mathlib.Order.Sublattice

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

English

For any M, ⊥.prod M = ⊥.

Русский

Для любого M, ⊥.prod M = ⊥.

LaTeX

$$(\\bot : Sublattice α).prod M = ⊥$$

Lean4

@[simp]
theorem bot_prod (M : Sublattice β) : (⊥ : Sublattice α).prod M = ⊥ :=
  SetLike.coe_injective empty_prod

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

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

Разделы

Аффилиация

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