Composition of implications - Lemmata Repository

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

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

Implications chain. This is the archive’s worked example: it shows the pieces an entry can use — numbered results, a diagram, a widget, a Mathlib corollary — on a result small enough to read at a glance.

Composing with self-implication ( $P \to P$ ) on either side changes nothing:

Main.lean

/-- Every proposition implies itself. -/
theorem self_implication (P : Prop) : P → P :=
  fun hp => hp

/-- Implications compose. -/
theorem implication_composition {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) : P → R :=
  fun hp => Lemmata.Shared.mp hqr (Lemmata.Shared.mp hpq hp)

/-- Composing with self-implication changes nothing. -/
theorem compose_self {P Q : Prop} (hpq : P → Q) : P → Q :=
  implication_composition (self_implication P) hpq

Try it: pick which hypotheses hold, and see whether $R$ follows.

Formal verification

✓ kernel-checked (Lean v4.35.0) Theorem 1 — Lemmata.ImplicationComposition.implication_composition (source)
✓ kernel-checked (Lean v4.35.0) Corollary 1 — Lemmata.ImplicationComposition.le_compose (source)

Checked at commit 29ff25c1aac1. The formal statement is machine-checked; that it matches the prose is checked by review. What “checked” means.