bot_lt_add

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithBot.bot_lt_add

English

In WithBot α, ⊥ < x + y is equivalent to ⊥ < x and ⊥ < y.

Русский

В WithBot α, ⊥ < x+y эквивалентно ⊥ < x и ⊥ < y.

LaTeX

$$$ ⊥ < x + y \\iff ⊥ < x \\land ⊥ < y $$$

Lean4

@[simp]
theorem bot_lt_add [LT α] : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y := by simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]

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

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

Разделы

Аффилиация

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