add_ne_bot

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

For WithBot α, x + y ≠ ⊥ iff x ≠ ⊥ and y ≠ ⊥.

Русский

Для слагаемой x и y в WithBot α, x+y ≠ ⊥ тогда и только тогда, когда x ≠ ⊥ и y ≠ ⊥.

LaTeX

$$$ x + y \\neq \\bot \\iff x \\neq \\bot \\land y \\neq \\bot $$$

Lean4

theorem add_ne_bot : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥ := by cases x <;> cases y <;> simp [← coe_add]

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

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

Разделы

Аффилиация

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