The logistic function as a two-term softmax

The share of one of two exponentials in their sum is the logistic function of the difference of their exponents, and the logistic function inverts the log-odds.

theorem Real.exp_div_add_exp_eq_sigmoid (x y : ℝ) : exp x / (exp x + exp y) = (x - y).sigmoid

The share of exp x in exp x + exp y is the logistic function of x - y.

theorem Real.sigmoid_log_div_one_sub {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) : (log (t / (1 - t))).sigmoid = t

The logistic function at the log-odds of a level in (0, 1) is that level.