User:Lord Farin
About me
Just a mathematics graduate with a broad interest, trying to make mathematics more accessible.
For you, reader
- Ever wondered how all those nice diagrams made it to your book? Check out the xymatrix package documentation.
- $\mathsf{Pr} \infty \mathsf{fWiki}$ comprises 42,221 proofs among 115,425 total pages, created by 759,960 edits in total.
Map of LF-Realm
My personal templates, sandboxes and the like:
User:Lord_Farin/Sandbox is my sandbox, which is used to test functionality, and prepare/attempt pages and structures. May have subpages attached.
User:Lord_Farin/SandboxTemplate is my sandbox template, in which I experiment with templates.
User:Lord Farin/Proof Structures is the place for proof templates I (and hopefully more people) tend to use.
User:Lord Farin/Tableau Proof Rules is where I keep templates for all allowed inferences in tableau proofs. This may appear as a bona fide page in the future.
User:Lord_Farin/Archive is a mixture between a graveyard and a safe haven for stuff which has nowhere else to go.
User:Lord_Farin/Backup documents old versions of pages I rebuilt from scratch.
User:Lord_Farin/Long-Term Projects is the place for things that are on even longer tracks than those in above Category; these are often meta-structural.
User:Lord_Farin/Books lists the books I have started to cover on PW.
Landmarks
I am particularly fond of the following contributions (all of which hence are my own work; i.e., I didn't copy the proof from some source):
- Absolutely Convergent Generalized Sum Converges
- Hilbert Space Direct Sum is Hilbert Space
- Definition:Magma of Sets, an encapsulating notion from my hand
Postponed
I promised (to myself or others) to get back at these points but the moment I do is so far in the future I would forget if they weren't here:
Too lazy / Loose ends
These results are mostly trivial and I can't be bothered putting them up right now; please, feel free.
- Generalize Zero and One are the only Consecutive Squares/Proof 2 to higher powers
- Definition:Characteristic Function Operation (the operation $\chi_{(\cdot)}$ sending a subset to its char. fn)
- Definition:Support Operation (the operation $\operatorname{supp}$ sending a function to its support)
- Support Operation Inverse to Characteristic Function Operation
- Inverse of Subset of Group is Inverse of Subset of Underlying Monoid (or some proper title)
Logic/Propositional Tableaus
- Definition:Used WFF / Definition:Unused WFF
- Fix inline definition on Tableau Extension Lemma
- Models for Propositional Logic
- Strongly Sound Proof System is Sound
- Strongly Complete Proof System is Complete
- Well-Formed Formula is Tautology iff Universal Closure is Tautology (that is, Universal Generalisation)
Natural Numbers
- Revisit:
- Equivalence of definitions of Natural Number Addition
- Definition for 1-based: Definition:Addition on 1-Based Natural Numbers
- Equivalence of definitions of ordering on $\N$
Follow-up projects
- Everything in Category:Natural Numbers needs a thorough review and possibly rewriting according to the new paradigm.
- Clear up Category:Natural Numbers/1-Based to a new, better category
Relation Theory
- weaker/stronger or some other description of subsets of relations.
- Definition:Difference of Relations
- Difference of Relations is Relation
Category Theory
- Projection Functor is Functor
- Domain Functor is Functor
- Codomain Functor is Functor
- Morphism Category is Category
- Composition Functor is Functor
- Slice Functor is Functor
- Coslice Category is Category
- Singleton Poset is Terminal Object
- Trivial Monoid is Initial Object, Trivial Monoid is Terminal Object
- Contravariant Representable Functor is Functor
- Category of Cones is Category
- Category of Cocones is Category
- Category of Groups is Category
- Limit of Singleton
- Functor to Product Category