mul_ne_bot — Mathlib

English

If a ≠ ⊥ and b ≠ ⊥ in WithBot α, then their product a*b ≠ ⊥. In other words, non-bottom elements remain non-bottom under multiplication.

Русский

Если a ≠ ⊥ и b ≠ ⊥ в WithBot α, то их произведение a*b ≠ ⊥. Иными словами, элементы не нижнего предела сохраняют своё свойство под умножением.

LaTeX

$$$\forall {a b : WithBot α}, (a \neq \bot) \land (b \neq \bot) \Rightarrow a*b \neq \bot$$$

Lean4

theorem mul_ne_bot {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a * b ≠ ⊥ :=
  WithTop.mul_ne_top (α := αᵒᵈ) ha hb

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