mul_ne_top — Mathlib

English

Let α be a type with DecidableEq and MulZeroClass. Then for any a,b in WithTop α with a ≠ ⊤ and b ≠ ⊤, their product a·b is not the top element.

Русский

Пусть α — тип с DecidableEq и MulZeroClass. Тогда для любых a,b ∈ WithTop α при a ≠ ⊤ и b ≠ ⊤ произведение a·b не равно ⊤.

LaTeX

$$$\\\\forall a,b \in \mathrm{WithTop}\\\\,\\\\alpha, a \\\\\\neq \\\\top \\\\rightarrow b \\\\neq \\\\top \\\\rightarrow a \\\\\\cdot b \\\\neq \\\\top$$$

Lean4

theorem mul_ne_top {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤ := by simp [mul_eq_top_iff, *]

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