Nat.two_pow_pos

theorem Nat.two_pow_pos : ∀ (w : ℕ), 0 < 2 ^ w

This theorem states that for any natural number `w`, the value of 2 raised to the power `w` is always greater than 0. In mathematical terms, for any $w \in \mathbb{N}$, $2^w > 0$.

More concisely: For all natural numbers $w$, $2^w > 0$.