No_Isomorphism_from_Woset_to_Initial_Segment

Proved

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

order-theoryproofwikiwell-ordered-sets

Let $\struct {S, \preceq}$ be a woset. Let $a \in S$ , and let $S_a$ be the initial segment of $S$ determined by $a$ . Then there is no order isomorphism between $S$ and $S_a$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem No_Isomorphism_from_Woset_to_Initial_Segment {S : Type _} [LinearOrder S] [IsWellOrder S (· < ·)] (a : S) : ¬∃ (f : S ≃o Set.Iio a), True := by sorry

Source

https://proofwiki.org/wiki/No_Isomorphism_from_Woset_to_Initial_Segment

View graph