English
Same as earlier: closure of s ∩ ℚ equals closure of s when s is ord-connected and nontrivial.
Русский
То же самое: замыкание s ∩ ℚ равно замыканию s, если s орд‑соединено и не тривиально.
LaTeX
$$$\overline{s \cap \mathbb{Q}} = \overline{s}$ for ord-connected $s$ nontrivial$$
Lean4
theorem closure_ordConnected_inter_rat {s : Set ℝ} (conn : s.OrdConnected) (nt : s.Nontrivial) :
closure (s ∩ .range Rat.cast) = closure s :=
(closure_mono inter_subset_left).antisymm <|
isClosed_closure.closure_subset_iff.mpr fun x hx ↦
Real.mem_closure_iff.mpr fun ε ε_pos ↦ by
have ⟨z, hz, ne⟩ := nt.exists_ne x
refine ne.lt_or_gt.elim (fun lt ↦ ?_) fun lt ↦ ?_
· have ⟨q, h₁, h₂⟩ := exists_rat_btwn (max_lt lt (sub_lt_self x ε_pos))
rw [max_lt_iff] at h₁
refine ⟨q, ⟨conn.out hz hx ⟨h₁.1.le, h₂.le⟩, q, rfl⟩, ?_⟩
simpa only [abs_sub_comm, abs_of_pos (sub_pos.mpr h₂), sub_lt_comm] using h₁.2
· have ⟨q, h₁, h₂⟩ := exists_rat_btwn (lt_min lt (lt_add_of_pos_right x ε_pos))
rw [lt_min_iff] at h₂
refine ⟨q, ⟨conn.out hx hz ⟨h₁.le, h₂.1.le⟩, q, rfl⟩, ?_⟩
simpa only [abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add'] using h₂.2
