eq_principalSeg — Mathlib

English

There is no nontrivial principal-segment embedding of a well-ordered set into itself; equivalently, no f : r ≺i r when r is a well-order.

Русский

Не существует ненулевого встраивания главного сегмента r в себя при условии, что r хорошо упорядочено.

LaTeX

$$$\\text{If }[\\text{IsWellOrder }\\alpha\\ r] \\, (f:\\ r \\prec_i r) \\Rightarrow \\text{False}$$$

Lean4

theorem _root_.InitialSeg.eq_principalSeg [IsWellOrder β s] (f : r ≼i s) (g : r ≺i s) (a : α) : g a = f a :=
  InitialSeg.eq g f a

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