div_ne_top — Mathlib

English

In the extended nonnegative reals, if x is not the top element and y is not zero, then x divided by y is not the top element.

Русский

В расширенных неотрицательных вещественных числах, если x ≠ ∞ и y ≠ 0, то x / y не равно ∞.

LaTeX

$$$\forall x,y \in \mathbb{R}_{\ge 0}^{\infty},\; x \neq \infty,\; y \neq 0 \Rightarrow \dfrac{x}{y} \neq \infty$$$

Lean4

@[aesop (rule_sets := [finiteness]) safe apply]
theorem div_ne_top {x y : ℝ≥0∞} (h1 : x ≠ ∞) (h2 : y ≠ 0) : x / y ≠ ∞ :=
  (div_lt_top h1 h2).ne

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