add_bot

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.add_bot

English

For every x in EReal, x + ⊥ = ⊥.

Русский

Для любого x из EReal выполняется x + ⊥ = ⊥.

LaTeX

$$$\\\\forall x \\\\in \\\\mathrm{EReal},\\\\ x + \\\\bot = \\\\bot$$$

Lean4

@[simp]
theorem add_bot (x : EReal) : x + ⊥ = ⊥ :=
  WithBot.add_bot _

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

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

Разделы

Аффилиация

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