lt_normThreshold_zero — Mathlib

English

If a > 0 and ha_pos is satisfied, then a/(1 − √2) < normThreshold(a,0).

Русский

Если a > 0 и выполняется ha_pos, тогда a/(1 − √2) < normThreshold(a,0).

LaTeX

$$$\\dfrac{a}{1-\\sqrt{2}} < \\operatorname{normThreshold}(a,0)$$$

Lean4

theorem lt_normThreshold_zero (ha_pos : 0 < a) : a / (1 - √2) < normThreshold a 0 :=
  by
  simp only [normThreshold_zero]
  calc
    a / (1 - √2)
    _ ≤ 0 := (div_nonpos_of_nonneg_of_nonpos ha_pos.le (by simp))
    _ < a := ha_pos

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