trans — Mathlib

English

If s cofinal in t and t cofinal in u, then s cofinal in u.

Русский

Если s кофинальное по отношению к t и t кофинальное по отношению к u, то s кофинальное по отношению к u.

LaTeX

$$$$ IsCofinalFor(s,t) \rightarrow IsCofinalFor(t,u) \rightarrow IsCofinalFor(s,u). $$$$

Lean4

protected theorem trans (hst : IsCoinitialFor s t) (htu : IsCoinitialFor t u) : IsCoinitialFor s u := fun _a ha ↦
  let ⟨_b, hb, hba⟩ := hst ha;
  let ⟨c, hc, hcb⟩ := htu hb;
  ⟨c, hc, hcb.trans hba⟩

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