trans — Mathlib

English

If p ~ q and q ~ r (ManyOneEquiv), then p ~ r.

Русский

Если p эквивалентно q и q эквивалентно r по ManyOneEquiv, то p эквивалентно r.

LaTeX

$$$\forall p\,q\,r,\ ManyOneEquiv\,p\,q\to ManyOneEquiv\,q\,r\to ManyOneEquiv\,p\,r$$$

Lean4

@[trans]
theorem trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
    ManyOneEquiv p q → ManyOneEquiv q r → ManyOneEquiv p r
  | ⟨pq, qp⟩, ⟨qr, rq⟩ => ⟨pq.trans qr, rq.trans qp⟩

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