Theorems · Theorem · logic and foundations

Ordinal.typein_le_typein

∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {a b : α},
  (Ordinal.typein r).toRelEmbedding a ≤ (Ordinal.typein r).toRelEmbedding b ↔ ¬r b a

Defined in

Mathlib.SetTheory.Ordinal.Basic

Cited by

3 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

IsWellOrder