instNonemptySeedRatReal — Mathlib

English

There exists a seed for the Hahn embedding from Rat M to Real M; in particular, HahnEmbedding.Seed Rat M Real is nonempty.

Русский

Существуем существование семени для Ханн-встраивания из Rat M в Real M; множество HahnEmbedding.Seed Rat M Real непусто.

LaTeX

$$$ \\exists s : HahnEmbedding.Seed \\mathbb{Q} \\, M \\, \\mathbb{R}, \\; \\text{True}$$$

Lean4

instance : Nonempty (HahnEmbedding.Seed ℚ M ℝ) :=
  by
  obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance
  choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)
  refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩
  apply Monotone.strictMono_of_injective
  · simpa using OrderHomClass.monotone (f c)
  · simpa using hf c

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