top_rel_top — Mathlib

English

For a principal-segment embedding f, and any a,b, the relation s b (f a) is equivalent to the existence of a' with f a' = b and r a' a.

Русский

Для встраивания f: s b (f a) эквивалентно существованию a', такого что f a' = b и r a' a.

LaTeX

$$$s\\ b\\ (f\\ a) \\iff \\exists a'\\ (f\\ a' = b \\land r\\ a'\\ a)$$$

Lean4

theorem top_rel_top {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} [IsWellOrder γ t] (f : r ≺i s) (g : s ≺i t)
    (h : r ≺i t) : t h.top g.top := by
  rw [Subsingleton.elim h (f.trans g)]
  apply PrincipalSeg.lt_top

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