Composition of implications - Lemmata Repository

Contributed by Sebastian Pokutta
First published 2026-10-19 · last changed 2026-10-20
License: CC BY 4.0

@misc{lemmata:2610.00001,
  title        = {Composition of implications},
  author       = {Sebastian Pokutta},
  howpublished = {Lemmata Repository, lemmata:2610.00001, \url{https://lemmata.iol.berlin/abs/2610.00001}},
  year         = {2026},
  url          = {https://lemmata.iol.berlin/abs/2610.00001},
  note         = {Version a9429cb9cbf5; formal statements checked in Lean 4}
}

Abstract. If $P \to Q$ and $Q \to R$ then $P \to R$ . The archive’s worked example: a result small enough to read at a glance, used to show numbered results, a diagram, an interactive widget and a Mathlib corollary.

Status¶

All formal results are kernel-checked with Lean v4.35.0. What “checked” means.

View the full entry → · category: Logic