Non-open infinite intersection of open sets.

nonopen.lean

import topology.algebra.ordered
import topology.metric_space.basic

-- Dê um exemplo de um espaço métrico `(X, d)` e uma família de subconjuntos
-- abertos `{Aᵢ | i ∈ I}` em `X`, tais que `⋂i ∈ I, Aᵢ` não é aberto.

-- Considere o espaço métrico `(X, d)` sendo `X = ℝ` e `d(x, y) := |x - y|`.

-- `f` é uma família infinita de conjuntos abertos em `ℝ` sendo
-- `fₙ := (-n⁻¹, n⁻¹)`.
@[simp] def f : ℕ → set ℝ :=
λ n, let N : ℝ := n + 1 in set.Ioo (-N⁻¹) N⁻¹

-- Cada conjunto `A = fₙ` é aberto por definição.
example : ∀ n, is_open (f n) :=
begin
  intro n,
  unfold f,
  exact is_open_Ioo,
end

lemma Inter_f : (⋂i, f i) = {0} :=
begin
  ext x,
  rw set.mem_Inter,
  split,
  { -- `⋂i, f i ⊇ {0}`
    -- p → q
    -- ¬ q → ¬ p
    contrapose!,
    intro hx,
    change x ≠ 0 at hx,
    rw ←abs_pos_iff at hx,
    obtain ⟨n, hn⟩ := exists_nat_one_div_lt hx,
    use n,
    simp only [f],
    rintro ⟨h₁, h₂⟩,
    simp only [one_div] at hn,
    rw lt_abs at hn,
    cases hn; linarith },
  { -- `⋂i, f i ⊆ {0}`
    intros hx n,
    change x = 0 at hx,
    simp only [f],
    rw set.mem_Ioo,
    rw hx,
    -- `∀ x, -x < 0 ↔ 0 < x`
    rw [neg_lt, neg_zero],
    rw and_self,
    rw inv_pos,
    have : 0 ≤ (n : ℝ), from nat.cast_nonneg n,
    linarith }
end

example : ¬ is_open (⋂i, f i) :=
begin
  rw Inter_f,
  rw metric.is_open_iff,
  intro h,
  specialize h 0 rfl,
  rcases h with ⟨ε, hε₁, hε₂⟩,
  specialize @hε₂ (ε/2),
  simp only [metric.mem_ball] at hε₂,
  simp only [dist] at hε₂,
  simp only [sub_zero] at hε₂,
  rw abs_of_pos (half_pos hε₁) at hε₂,
  specialize hε₂ (half_lt_self hε₁),
  change _ = _ at hε₂,
  linarith
end