mul_eq_bot_iff — Mathlib

English

For a,b ∈ WithBot α, the product a*b equals the bottom element ⊥ if and only if exactly one of a,b is bottom and the other is not bottom. Equivalently, a*b = ⊥ ⇔ (a ≠ ⊥ ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ ⊥).

Русский

Для a, b ∈ WithBot α произведение a·b равно нижнему элементу ⊥ тогда и только тогда, когда ровно один из множителей равен ⊥, а другой не равен ⊥. Иными словами, a·b = ⊥ iff (a ≠ ⊥ ∧ b = ⊥) ∨ (a = ⊥ ∧ b ≠ ⊥).

LaTeX

$$$ a*b = \bot \iff (a \neq \bot \\land b = \bot) \\lor (a = \bot \\land b \neq \bot) $$$

Lean4

theorem mul_eq_bot_iff : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0 := by rw [mul_def]; aesop

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