instInfiniteOfModelDloOrderOfNonempty

English

Any nonempty model of dense linear orders is infinite.

Русский

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

LaTeX

$$$ \text{Infinite } M $$$

Lean4

instance (M : Type w) [Language.order.Structure M] [M ⊨ Language.order.dlo] [Nonempty M] : Infinite M :=
  by
  letI := orderStructure ℚ
  obtain ⟨f, _⟩ := embedding_from_cg cg_of_countable default (dlo_isExtensionPair ℚ M)
  exact Infinite.of_injective f f.injective

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