integers are closed in reals

Stream: Is there code for X?

[Bhavik Mehta]

import topology.instances.real

example : is_closed {x : ℝ | ∃ (z : ℤ), x = z} :=
begin
  sorry
end

Is there a statement like this in mathlib somewhere?

[Adam Topaz]

It's called is_closed.eq or something like that... Works with t2 instance

[Bhavik Mehta]

docs#is_closed_eq

[Adam Topaz]

Ah wait not quite, but should be easy with that

[Bhavik Mehta]

I don't think that applies here -- right

[Adam Topaz]

Oh that's a Z, sorry yeah that's a bit different

[Adam Topaz]

Presumably the correct formulation is to have a closed embedding from Z to R

[Bhavik Mehta]

Here's how I ended up doing it:

example : is_closed {x : ℝ | ∃ (z : ℤ), x = z} :=
begin
  rw ←is_open_compl_iff,
  have : {x : ℝ | ∃ (z : ℤ), x = z}ᶜ = ⋃ (z : ℤ), Ioo z (z+1),
  { ext,
    simp only [not_exists, mem_Union, mem_Ioo, mem_set_of_eq, mem_compl_eq],
    split,
    { intro q,
      refine ⟨floor x, lt_of_le_of_ne (floor_le x) (ne.symm (q _)), _⟩,
      apply lt_floor_add_one },
    { rintro ⟨z, hz₁, hz₂⟩ y rfl,
      norm_cast at hz₁ hz₂,
      linarith } },
  rw this,
  exact is_open_Union (λ i, is_open_Ioo),
end

[Patrick Massot]

I wanted to have a quick look at Zulip before resuming work after dinner. I saw this. I thought I should do it properly. Then I found a couple of API holes (also called rabbit holes). One hour later...

import topology.instances.real

open_locale topological_space uniformity

open filter uniform_space set

lemma uniform_space.mem_closure_iff_symm_ball  {X : Type*} [uniform_space X] {s : set X} {x} :
  x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 X → symmetric_rel V → (s ∩ ball x V).nonempty :=
begin
  simp [mem_closure_iff_nhds_basis (has_basis_nhds x)],
  tauto,
end

lemma uniform_space.mem_closure_iff_ball  {X : Type*} [uniform_space X] {s : set X} {x} :
  x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 X → (ball x V ∩ s).nonempty :=
begin
  simp_rw [mem_closure_iff_nhds, mem_nhds_iff],
  split,
  { intros h V V_in,
    exact h (ball x V) ⟨V, V_in, subset.refl _⟩ },
  { rintros h t ⟨V, V_in, Vt⟩,
    exact nonempty.mono (inter_subset_inter_left s Vt) (h V_in) },
end

lemma eq_of_uniformity {X : Type*} [uniform_space X] [separated_space X] {x y : X}
  (h : ∀ {V}, V ∈ 𝓤 X → (x, y) ∈ V) : x = y :=
separated_def.mp ‹separated_space X› x y (λ _, h)

lemma eq_of_uniformity_basis {X : Type*} [uniform_space X] [separated_space X] {ι : Type*}
  {p : ι → Prop} {s : ι → set (X × X)} (hs : (𝓤 X).has_basis p s) {x y : X}
  (h : ∀ {i}, p i → (x, y) ∈ s i) : x = y :=
eq_of_uniformity (λ V V_in, let ⟨i, hi, H⟩ := hs.mem_iff.mp V_in in H (h hi))

lemma eq_of_forall_symmetric {X : Type*} [uniform_space X] [separated_space X] {x y : X}
  (h : ∀ {V}, V ∈ 𝓤 X → symmetric_rel V → (x, y) ∈ V) : x = y :=
eq_of_uniformity_basis has_basis_symmetric (by simpa [and_imp] using λ _, h)

open uniform_space

lemma ball_inter_left {β : Type*} (x : β) (V W : set (β × β)) : ball x (V ∩ W) ⊆ ball x V :=
ball_mono (inter_subset_left V W) x

lemma ball_inter_right {β : Type*} (x : β) (V W : set (β × β)) : ball x (V ∩ W) ⊆ ball x W :=
ball_mono (inter_subset_right V W) x

lemma is_closed_of_spaced_out {X : Type*} [uniform_space X] [separated_space X] {V₀ : set (X × X)}
  (V₀_in : V₀ ∈ 𝓤 X) {s : set X} (hs : ∀ {x y}, x ∈ s → y ∈ s → (x, y) ∈ V₀ → x = y) :
is_closed s :=
begin
  rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩,
  apply is_closed_of_closure_subset,
  intros x hx,
  rw [mem_closure_iff_ball] at hx,
  rcases hx V₁_in with ⟨y, hy, hy'⟩,
  suffices : x = y, by rwa this,
  apply eq_of_forall_symmetric,
  intros V V_in V_symm,
  rcases hx (inter_mem_sets V₁_in V_in) with ⟨z, hz, hz'⟩,
  suffices : z = y,
  { rw ← this,
    exact ball_inter_right x _ _ hz },
  exact hs hz' hy' (h_comp $ mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
end

example : is_closed {x : ℝ | ∃ n : ℤ, x = n} :=
begin
  refine is_closed_of_spaced_out (metric.uniformity_basis_dist.mem_of_mem $ one_half_pos) _,
  rintros - - ⟨p, rfl⟩ ⟨q, rfl⟩ (h : abs (p - q : ℝ) < 1/2),
  norm_cast at *,
  /-
  p q : ℤ,
  h : (abs (p - q) : ℝ) < 1 / 2
  ⊢ p = q
  -/
  sorry
end

[Damiano Testa]

If I remember correctly, there is a lemma that says that an integer of absolute value less than one is zero, though it might be for nat.abs. I'm on mobile, though

[Patrick Massot]

I certainly hope this sorry is provable. But I have no interest at all in proving it. All the fun is above the example.

[Damiano Testa]

Sure, I just felt proud, since I think that the lemma about abs was my first PRed simp lemma! :upside_down:

[Damiano Testa]

https://leanprover-community.github.io/mathlib_docs/data/int/basic.html#int.eq_zero_iff_abs_lt_one

[Damiano Testa]

You never forget your first simp lemma...

[Patrick Massot]

example : is_closed {x : ℝ | ∃ n : ℤ, x = n} :=
begin
  refine is_closed_of_spaced_out (metric.uniformity_basis_dist.mem_of_mem $ zero_lt_one) _,
  rintros - - ⟨p, rfl⟩ ⟨q, rfl⟩ (h : abs (p - q : ℝ) < 1),
  norm_cast at *,
  exact eq_of_sub_eq_zero (int.eq_zero_iff_abs_lt_one.mp h)
end

[Patrick Massot]

Indeed it does the job

[Patrick Massot]

Note that I opened #7538 containing all preliminaries for the above proof.

[Bhavik Mehta]

Nice! I also used docs#int.eq_zero_iff_abs_lt_one for similar proofs :D