Order_Isomorphism_from_Woset_onto_Subset

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 $T \subseteq S$ . Let $f: S \to T$ be an order isomorphism. Then $\forall x \in S: x \preceq \map f x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Order_Isomorphism_from_Woset_onto_Subset {S : Type _} [LinearOrder S] [IsWellOrder S (· < ·)] (f : S → S) (hf : StrictMono f) : ∀ x, f x ≥ x := by sorry

Source

https://proofwiki.org/wiki/Order_Isomorphism_from_Woset_onto_Subset

View graph