embedReal_one — Mathlib

English

Let M be an Archimedean ordered additive monoid with 1. Then the Archimedean embedding embeds M into the real numbers so that (embedReal M)(1) = 1.

Русский

Пусть M — Архимедово упорядоченное аддитивное моноид с единицей; отображение embedReal M отображает 1 в 1.

LaTeX

$$$(\operatorname{embedReal} M)(1) = 1$$$

Lean4

@[simp]
theorem embedReal_one : (embedReal M) 1 = 1 := by
  rw [embedReal_apply]
  apply le_antisymm
  · apply csSup_le (ratLt'_nonempty 1)
    suffices ∀ (x : ℚ), x.num • (1 : M) < (x.den : ℤ) • (1 : M) → (x : ℝ) ≤ 1 by simpa using this
    intro x hx
    suffices x ≤ 1 by norm_cast
    simpa [Rat.le_iff] using ((smul_lt_smul_iff_of_pos_right zero_lt_one).mp hx).le
  · rw [le_csSup_iff (ratLt'_bddAbove (1 : M)) (ratLt'_nonempty 1)]
    simp_rw [mem_upperBounds]
    suffices ∀ (x : ℝ), (∀ (y : ℚ), y.num • (1 : M) < (y.den : ℤ) • 1 → y ≤ x) → 1 ≤ x by simpa using this
    intro x h
    have h' (y : ℚ) (hy : y < 1) : y ≤ x :=
      h _ ((smul_lt_smul_iff_of_pos_right zero_lt_one).mpr (by simpa using (Rat.lt_iff _ _).mp hy))
    contrapose! h'
    obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
    exact ⟨y, (by norm_cast at hy), hxy⟩

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