bot_prod

Mathlib.Order.UpperLower.Prod

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

English

The product with bottom in the second factor is bottom: ⊥ ×ˢ t = ⊥.

Русский

Произведение с нулём во второй компоненте равно нулю: ⊥ ×ˢ t = ⊥.

LaTeX

$$$ (\bot) \times^{\mathrm{S}} t = \bot $$$

Lean4

@[simp]
theorem bot_prod : (⊥ : LowerSet α) ×ˢ t = ⊥ :=
  ext empty_prod

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

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

Разделы

Аффилиация

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