transitive_oneOneReducible — Mathlib

English

For predicates p, q, r, if p ≤₁ q and q ≤₁ r, then p ≤₁ r.

Русский

Для предикатов p, q, r: если p ≤₁ q и q ≤₁ r, то p ≤₁ r.

LaTeX

$$$\forall \alpha\beta\gamma\,[Primcodable\ \alpha]\,[Primcodable\ \beta]\,[Primcodable\ \gamma]\{p:\alpha\to\mathrm{Prop}\}\{q:\beta\to\mathrm{Prop}\}\{r:\gamma\to\mathrm{Prop}\},\ p\le_1 q\to q\le_1 r\to p\le_1 r$$$

Lean4

theorem transitive_oneOneReducible {α} [Primcodable α] : Transitive (@OneOneReducible α α _ _) := fun _ _ _ =>
  OneOneReducible.trans

Похожие утверждения