Hi Jay. This is great. Python is one of my favorite languages, so this is a good resource. I will certainly go through this in some depth. Thanks!
I happened to run into the "SRC Technical Note - The Operators of TLA+" and encountered another explanation of this notation "[x \in D |-> e]" as being TLA's equivalent to lambda expressions. Then it clicked for me a little more as this being a function generator.
In TLA+:
f = [x \in Nat |-> x^2 ]
In Python:
f = lamba x: x**2
I liked your take on that as well using a list comprehension. function == array mapping makes sense, but tough to break out of the programming mindset. Even Lamport seems to mix and match terms like "array _expression_" with "function" in his videos. I'm not yet able to "translate" synonymous terminology on the fly :)