coe_add_eq_bot_iff

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

For any a, y : WithBot α and b : α, a + y = ⊥ iff y = ⊥.

Русский

Для любых a, y : WithBot α и b : α, a + y = ⊥ тогда и только тогда, когда y = ⊥.

LaTeX

$$$ a + y = \\bot \\iff y = \\bot $$$

Lean4

theorem coe_add_eq_bot_iff : a + y = ⊥ ↔ y = ⊥ := by simp

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

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

Разделы

Аффилиация

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