been playing with some math notation recently
a function f is surjective iff for every y ∈ cod(f) we have

turns out there is a pretty natural way modify this notation to support ∀∃-statements instead of just ∀-statements. using it, topological continuity looks like this:
(edit: this is not the definition of continuity, oops)
further, you can actually manage alternating quantifiers in some cases, but it's not necessarily readable...
here's epsilon-delta. lim_(x → x₀) f(x) = L iff

as a reminder, epsilon-delta in traditional form is this:
lim_(x → x₀) f(x) = L iff (∀ε > 0)(∃δ > 0)(∀x)( x ∈ B_δ(x₀) ⇒ f(x) ∈ B_ε(L) )
here by Bₐ(z) i mean the open ball of size a around z; that is, the interval (z - a, z + a)
ok, so how does the diagram given correspond to this sentence? let's first give the bullets some variable names
a by-the-books reading of this diagram wants to start with "for all ε and x such that ..." since both ε and x are solid bullets. but if we try to finish that sentence we'll fail, since x is constrained by the requirement x ∈ B_δ(x₀) which references the as-of-yet unquantified variable δ
so since x is constrained by δ, then it must be that δ is quantified above x. if we allow for that variable swap then our sentence instead starts with "for all ε such that ... exists δ such that ... forall x ..." which matches up with what epsilon-delta does actually say
there's some worries to be had regarding allowing quantifier swaps. originally we knew order of quantifiers because it was always ∀∃, by definition. but if we allow quantifier swaps now order of quantifiers could be ambiguous!
one resolution to this is as follows: you are allowed to apply only the minimal set of quantifier swaps needed to ensure that all variables are able to reference variables which constrain them. (as we did with the above diagram)
if we really wanted to adopt this convention we'd have to prove some level of coherence, that either (a) whenever swapping is required there is only one minimal set of valid swaps; or (b) there are multiple, but they produce equivalent sentences. idk if this is actually true or not. at least for the above diagram nothing bad happens!
