coe_add_eq_top_iff

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

For a ∈ α and y ∈ WithTop α, a + y = ⊤ iff y = ⊤.

Русский

Для a ∈ α и y ∈ WithTop α, a + y = ⊤ эквивалентно y = ⊤.

LaTeX

$$$a + y = \\top \\iff y = \\top$$$

Lean4

theorem coe_add_eq_top_iff : a + y = ⊤ ↔ y = ⊤ := by simp

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

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

Разделы

Аффилиация

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