isSt_sSup — Mathlib

English

For finite x, the standard part equals the real supremum of reals below x.

Русский

Для конечного x стандартная часть равна реально-верхней грани множества чисел ниже x.

LaTeX

$$IsSt x (sSup \\{ y : \\mathbb{R} \\mid (y : \\mathbb{R}^*) < x \\})$$

Lean4

theorem isSt_sSup {x : ℝ*} (hni : ¬Infinite x) : IsSt x (sSup {y : ℝ | (y : ℝ*) < x}) :=
  let S : Set ℝ := {y : ℝ | (y : ℝ*) < x}
  let R : ℝ := sSup S
  let ⟨r₁, hr₁⟩ := not_forall.mp (not_or.mp hni).2
  let ⟨r₂, hr₂⟩ := not_forall.mp (not_or.mp hni).1
  have HR₁ : S.Nonempty := ⟨r₁ - 1, lt_of_lt_of_le (coe_lt_coe.2 <| sub_one_lt _) (not_lt.mp hr₁)⟩
  have HR₂ : BddAbove S := ⟨r₂, fun _y hy => le_of_lt (coe_lt_coe.1 (lt_of_lt_of_le hy (not_lt.mp hr₂)))⟩
  fun δ hδ =>
  ⟨lt_of_not_ge fun c =>
      have hc : ∀ y ∈ S, y ≤ R - δ := fun _y hy => coe_le_coe.1 <| le_of_lt <| lt_of_lt_of_le hy c
      not_lt_of_ge (csSup_le HR₁ hc) <| sub_lt_self R hδ,
    lt_of_not_ge fun c =>
      have hc : ↑(R + δ / 2) < x := lt_of_lt_of_le (add_lt_add_left (coe_lt_coe.2 (half_lt_self hδ)) R) c
      not_lt_of_ge (le_csSup HR₂ hc) <| (lt_add_iff_pos_right _).mpr <| half_pos hδ⟩

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