closure_of_rat_image_lt — Mathlib

English

The closure of the image of rationals under casting into ℝ of x>q is {r ∈ ℝ | q ≤ r}.

Русский

Замыкание образа рационала через отображение в ℝ для q равно {r ∈ ℝ | q ≤ r}.

LaTeX

$$$\overline{(\mathbb{Q} \overset{\text{cast}}{\to} \mathbb{R})[\{x\mid q

Lean4

theorem closure_of_rat_image_lt {q : ℚ} : closure (((↑) : ℚ → ℝ) '' {x | q < x}) = {r | ↑q ≤ r} :=
  by
  convert closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1
  · congr!; aesop
  · exact (closure_Ioi _).symm
  ·
    exact
      ⟨q + 1, show (q : ℝ) < _ by linarith, q + 2, show (q : ℝ) < _ by linarith, by simp⟩
        /- TODO(Mario): Put these back only if needed later
        lemma closure_of_rat_image_le_eq {q : ℚ} : closure ((coe : ℚ → ℝ) '' {x | q ≤ x}) = {r | ↑q ≤ r} :=
          _

        lemma closure_of_rat_image_le_le_eq {a b : ℚ} (hab : a ≤ b) :
            closure (of_rat '' {q:ℚ | a ≤ q ∧ q ≤ b}) = {r:ℝ | of_rat a ≤ r ∧ r ≤ of_rat b} :=
          _
        -/

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