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

bullets signify values that we haven't given a name to; a diagram with a bullet corresponds to an existential formula. arrows signify relations. the ↦ arrow is used for functions, so x ↦f y means f(x) = y
a function f is injective iff for every distinct x, y ∈ dom(f) we have
i like these diagrams. they're neat. and fun. also, in some cases i think they can really help clarity. i have a proof thats ~1 paragraph in traditional style and ~2 lines with diagrams
given a relation ⇝ ⊆ A², its transitive closure is the relation R so that xRy iff
writing conditions this way feels almost akin to doing point-free programming. eg eliminating variable names, exposing underlying structure
a function f : (X, τ) → (Y, σ) between topological spaces is continuous iff for every x ∈ X and f(x) ∋ V ∈ σ we have
(edit: this is not the definition of continuity, oops)
it's tempting to want to fit entire sentences into a diagram, including e.g. alternating quantifiers. i don't know of a good way to do it though. im sticking to existentials only for now
we say two categories C and D are equivalent iff
one interesting thing i have done is use double-struck arrows for implication and dotted arrows for implied arrows. for instance an order (A, ≤) is dense iff for all a, b ∈ A we have
here's a proof that ⊆ is transitive:
finally, a larger proof. take two relations over a set A and call them ↪ and ↠. assume that ↠ is transitive and assume that if A ↠ B ↪ C then
now define a relation R so that xRy iff x ↪ • ↪ • ↪ ⋯ ↪ • ↠ y. then R is transitive:
writing this proof (and problem statement!) in traditional style would require the works, including explicit invocation of induction. but with a diagram? blam, boom, ur done
in fairness the proof does lack clarity, like where/how precisely we use our assumptions
(btw, this seemingly-contrived setup actually comes from an organic scenario!)
