mul_lt_top

Mathlib.Algebra.Order.Ring.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.mul_lt_top

← MathLib Explorer

English

Let a,b ∈ WithTop α with a < ⊤ and b < ⊤. Then a·b < ⊤.

Русский

Пусть a,b ∈ WithTop α и a < ⊤, b < ⊤. Тогда a·b < ⊤.

LaTeX

$$$\\\\forall a,b \in \\mathrm{WithTop}\\\\,\\\\alpha, a < \\top \\\\rightarrow b < \\top \\\\rightarrow a \\\\cdot b < \\top$$$

Lean4

theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ :=
  by
  rw [WithTop.lt_top_iff_ne_top] at *
  exact mul_ne_top ha hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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