trans — Mathlib

English

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

Русский

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

LaTeX

$$$$ IsCofinalFor(s,t) \land IsCofinalFor(t,u) \Rightarrow IsCofinalFor(s,u). $$$$

Lean4

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

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