coe_mul_bot_of_pos — Mathlib

English

Let x be a real number with x > 0. Then the product of x (viewed inside the extended real system) with the bottom element equals the bottom element; i.e., x * ⊥ = ⊥ in EReal.

Русский

Пусть x ∈ ℝ и x > 0. Тогда произведение x (встроенное в расширенные вещественные) на нижнюю границу равняется нижней границе: x * ⊥ = ⊥ в EReal.

LaTeX

$$$0 < x \implies (x\text{ as EReal}) \cdot \perp = \perp$$$

Lean4

theorem coe_mul_bot_of_pos {x : ℝ} (h : 0 < x) : (x : EReal) * ⊥ = ⊥ :=
  if_pos h

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