nonempty_orderEmbedding_of_finite_infinite

English

Any finite linear order can be order-embedded into any infinite linear order.

Русский

Любой конечный линейный порядок может быть встраен в любой бесконечный линейный порядок.

LaTeX

$$nonempty (OrderEmbedding α β)$$

Lean4

/-- Any finite linear order order-embeds into any infinite linear order. -/
theorem nonempty_orderEmbedding_of_finite_infinite (α : Type*) [LinearOrder α] [hα : Finite α] (β : Type*)
    [LinearOrder β] [hβ : Infinite β] : Nonempty (α ↪o β) :=
  by
  haveI := Fintype.ofFinite α
  obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq β (Fintype.card α)
  exact ⟨((Fintype.orderIsoFinOfCardEq α rfl).symm.toOrderEmbedding).trans (s.orderEmbOfFin hs)⟩

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