Normality on nets from normality on sequences, via a strictly monotone L

Suppose L is monotone and strictly monotone on projections (p ≤ q and L q ≤ L p imply p = q, e.g. a faithful additive dimension or trace) and L f_n → L(sup f_n) for increasing sequences. Then L e_i → L(sup e_i) for every increasing net. Proof: choose indices i_0 ≤ i_1 ≤ ... with L(e_{i_n}) → s = sup_i L(e_i), built with Nat.rec as a_{n+1} = a_n ⊔ j_{n+1}, and let F be their sup. For any fixed i, the sequence e_{a_n ⊔ i} has sup G ≥ F, and L G = s = L F by squeezing, so G = F and e_i ≤ F. Hence sup e_i = F. In Lean this keeps the general net statement free of countable decomposability. Sequence normality comes from countable additivity by summing the differences g(n+1) − g(n), where g 0 = 0 and g (n+1) = f n is written as Nat.rec so that g (n+1) reduces to f n by rfl.