exists_orderAddMonoidHom_real_injective

English

There exists an injective order-preserving monoid hom f : M → ℝ.

Русский

Существует инъективное дополнительно упорядоченное моноид-гомоморфное отображение f: M → ℝ.

LaTeX

$$$\exists f: M \to_+^o \mathbb{R}, \; \text{Injective}(f)$$$

Lean4

theorem exists_orderAddMonoidHom_real_injective : ∃ f : M →+o ℝ, Function.Injective f :=
  by
  cases subsingleton_or_nontrivial M
  · exact ⟨0, Function.injective_of_subsingleton _⟩
  · obtain ⟨a, ha⟩ := exists_ne (0 : M)
    let one : One M := ⟨|a|⟩
    have : ZeroLEOneClass M := ⟨abs_nonneg a⟩
    have : NeZero (1 : M) := ⟨abs_ne_zero.mpr ha⟩
    exact ⟨embedReal M, embedReal_injective M⟩

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