Cofinite topology.

cofinite.lean

import topology.order

variables {α : Type*}

namespace cofinite

@[simp] def is_open : set α → Prop :=
λ s, set.finite sᶜ ∨ s = ∅

lemma is_open_univ : is_open (set.univ : set α) :=
begin
  unfold is_open,
  left,
  rw set.compl_univ,
  exact set.finite_empty
end

lemma is_open_inter (s₁ s₂ : set α) :
  is_open s₁ → is_open s₂ → is_open (s₁ ∩ s₂) :=
begin
  rintros (hs₁ | hs₁) (hs₂ | hs₂),
  { unfold is_open,
    left,
    rw set.compl_inter,
    exact set.finite.union hs₁ hs₂ },
  all_goals { right, simp [hs₁, hs₂] }
end

lemma is_open_sUnion (s : set (set α)) (hs : ∀ t, t ∈ s → is_open t) :
  is_open (⋃₀ s) :=
begin
  by_cases h : ∃ t, t ∈ s ∧ t ≠ ∅,
  { unfold is_open,
    left,
    rcases h with ⟨t, ht₁, ht₂⟩,
    have ht₂ : set.finite tᶜ,
    { cases hs t ht₁ with ht₃ ht₃,
      { exact ht₃ },
      { exfalso, exact ht₂ ht₃ } },
    apply set.finite.subset ht₂,
    intros x hx,
    suffices : x ∉ t, by simpa,
    simp at hx,
    change ∀ t', _ at hx,
    exact hx t ht₁ },
  { push_neg at h,
    unfold is_open,
    right,
    ext x,
    suffices : ∀ t, t ∈ s → x ∉ t, by simpa,
    intros t ht,
    specialize h t ht,
    rw set.eq_empty_iff_forall_not_mem at h,
    exact h x }
end

@[simp] instance topological_space (α : Type*) : topological_space α :=
{ is_open := is_open,
  is_open_univ := is_open_univ,
  is_open_inter := is_open_inter,
  is_open_sUnion := is_open_sUnion }

lemma discrete_of_fintype [fintype α] : discrete_topology α :=
begin
  constructor,
  ext s,
  split; intro hs,
  { trivial },
  { left, apply set.finite.of_fintype }
end

example : ⋃₀∅ = (∅ : set α) :=
begin
  exact set.sUnion_empty
end

example :
  cofinite.topological_space α = topological_space.generate_from {s | ∃! x, x ∉ s} :=
begin
  ext s,
  simp only [cofinite.topological_space, topological_space.generate_from],
  split,
  { rintro (hs | rfl),
    { -- Special thanks for Mario Carneiro for this nice little proof.
      -- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Finite.20set.20induction.20and.20complement
      convert @is_open_bInter _ _ (topological_space.generate_from {s | ∃! x, x ∉ s}) _
        (λ x, ({x} : set α)ᶜ) hs _,
      { ext x, simp [not_imp_not] },
      { intros x _,
        apply topological_space.generate_open.basic,
        use x, simp } },
    { rw ←set.sUnion_empty,
      apply topological_space.generate_open.sUnion,
      intros s hs,
      exfalso,
      exact set.not_mem_empty s hs } },
  { intro hs,
    induction hs with s hs _ _ _ _ ih₁ ih₂ _ _ ih,
    { rcases hs with ⟨x, hx₁, hx₂⟩,
      suffices : sᶜ = {x},
      { left, rw this, exact set.finite_singleton x },
      ext y,
      split,
      { exact hx₂ y },
      { intro hy,
        change y = x at hy,
        rwa hy } },
    { left, simp },
    { exact is_open_inter _ _ ih₁ ih₂ },
    { exact is_open_sUnion _ ih } }
end

end cofinite