Isomorphic_Ordinals_are_Equal

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

ordinalsproofwikiset-theory

Let $A$ and $B$ be ordinals that are order isomorphic. Then $A = B$ .

Preamble

import Mathlib.SetTheory.Ordinal.Basic

Formal statement

theorem Isomorphic_Ordinals_are_Equal (a b : Ordinal) (h : a ≤ b) (h2 : b ≤ a) : a = b := by sorry

Source