pos_denom — Mathlib

English

For all x, the denominator expNegInvGlue(x) + expNegInvGlue(1 - x) is strictly positive.

Русский

Для всех x знаменатель expNegInvGlue(x) + expNegInvGlue(1 - x) положителен строго.

LaTeX

$$$0 < \expNegInvGlue(x) + \expNegInvGlue(1 - x)$$$

Lean4

theorem pos_denom (x) : 0 < expNegInvGlue x + expNegInvGlue (1 - x) :=
  (zero_lt_one.gt_or_lt x).elim (fun hx => add_pos_of_pos_of_nonneg (pos_of_pos hx) (nonneg _)) fun hx =>
    add_pos_of_nonneg_of_pos (nonneg _) (pos_of_pos <| sub_pos.2 hx)

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