add_top

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.add_top

English

Adding top on the right yields top: x + ⊤ = ⊤.

Русский

Сложение сверху справа даёт ⊤: x + ⊤ = ⊤.

LaTeX

$$$\\\\forall x \\\\in \\\\mathrm{PartENat}, x + \\\\top = \\\\top$$$

Lean4

theorem add_top (x : PartENat) : x + ⊤ = ⊤ := by rw [add_comm, top_add]

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

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

Разделы

Аффилиация

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