exists_domain_eq_top — Mathlib

English

There exists a partial Hahn embedding whose domain is the top submodule.

Русский

Существует частичное Ган-встраивание, домен которого равняется верхнему подмножеству.

LaTeX

$$$\\exists f : Partial seed, f.val.domain = Submodule.instTop.top$$$

Lean4

/-- There exists a `HahnEmbedding.Partial` whose domain is the whole module. -/
theorem exists_domain_eq_top [IsOrderedAddMonoid R] [Archimedean R] : ∃ f : Partial seed, f.val.domain = ⊤ :=
  by
  obtain ⟨f, hf⟩ := exists_isMax seed
  refine ⟨f, Submodule.eq_top_iff'.mpr ?_⟩
  rw [isMax_iff_forall_not_lt] at hf
  contrapose! hf with hx
  obtain ⟨x, hx⟩ := hx
  exact ⟨f.extend hx, f.lt_extend hx⟩

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