typein_le_typein — Mathlib

English

For any well-ordered α, the order-embedding of a into b exists iff type(a) ≤ type(b) without relations aRb.

Русский

Для любого хорошо упорядоченного α существует вложение типа a в b тогда и только тогда, когда type(a) ≤ type(b) без учета отношения aRb.

LaTeX

$$$\forall {\alpha},{\beta},\ {r},{s}\ [IsWellOrder\ \alpha r]\ [IsWellOrder\ \beta s],\\ Iff( le( type(r), type(s) ), Nonempty(RelEmbedding r s))$$

Lean4

@[simp]
theorem typein_le_typein (r : α → α → Prop) [IsWellOrder α r] {a b : α} : typein r a ≤ typein r b ↔ ¬r b a := by
  rw [← not_lt, typein_lt_typein]

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