A proof of Baire category theorem using #2850

Stream: maths

[David Wärn]

In an attempt to better explain the point of PR #2850, here is a proof of BCT for a complete metric space X (of course there is already a shorter proof in mathlib). The idea is to consider the poset of closed subsets C of X with nonempty interior, ordered by reverse inclusion. We have two families of predicates on this poset: one saying "C has diameter <= r", and one saying "C is a subset of S". We separately show that these predicates are both "cofinal", in the sense that any C can be shrunk so as to satisfy the predicate, assuming r > 0 and S open dense, respectively. #2850 finishes the job, more or less.

import order.generic_cofilter
import analysis.specific_limits

/- This is an attempt at illustrating the use #2850.

-/

open metric set

variables {α : Type*} [metric_space α]

-- where can I find this lemma?
lemma closed_ball_subset_ball (x : α) {a b : ℝ} (h : a < b) :
  closed_ball x a ⊆ ball x b :=
λ y hy, calc dist y x ≤ a : hy
                  ... < b : h

-- where can I find this lemma?
lemma metric_space_is_regular (x : α) (s : set α) (ho : is_open s) (xs : x ∈ s) :
  ∃ t : set α, is_open t ∧ x ∈ t ∧ closure t ⊆ s :=
begin
  rcases metric.is_open_iff.mp ho x xs with ⟨r, rpos, xrs⟩,
  refine ⟨ball x (r/2), is_open_ball, mem_ball_self (half_pos rpos), _⟩,
  calc closure (ball x (r/2)) ⊆ closed_ball x (r/2) : closure_ball_subset_closed_ball
                          ... ⊆ ball x r : closed_ball_subset_ball x (half_lt_self rpos)
                          ... ⊆ s : xrs
end

variable (α)
/-- The type of closed subsets of `α` with nonempty interior. -/
def cniset : Type _ :=
  { C : set α // is_closed C ∧ (interior C).nonempty }
variable {α}

/-- We order cnisets by reverse inclusion. A smaller cniset is thought of as
    'extending' a larger set, because it imposes more constraints. -/
instance : preorder (cniset α) :=
{ le := λ f g, g.val ⊆ f.val,
  le_refl := by tidy, le_trans := by tidy, }

/-- Given a dense open set `s`, any cniset can be shrunk so as to lie in `s`. -/
def cofinal_of_dense (s : set α) (ho : is_open s) (hd : closure s = univ) :
  { D : set (cniset α) // cofinal D } :=
{ val := { f | f.val ⊆ s},
  property :=
    begin
      rintros ⟨C, hc, hni⟩,
      rcases dense_iff_inter_open.mp hd (interior C) (is_open_interior) hni
        with ⟨x, xic, xs⟩,
      rcases metric_space_is_regular x (s ∩ interior C) (is_open_inter ho $ is_open_interior)
        ⟨xs, xic⟩ with ⟨t, hto, xt, ht⟩,
      rw subset_inter_iff at ht,
      refine ⟨⟨closure t, is_closed_closure, _⟩, _, _⟩,
      { use x,
        rw mem_interior,
        exact ⟨t, subset_closure, hto, xt⟩, },
      exact ht.1,
      calc closure t ⊆ interior C : ht.2
                 ... ⊆ C : interior_subset
    end }

/-- Given `r > 0`, any cniset can be shrunk so as to have diameter `≤ r`:
    simply pick a point in the interior and intersect with the `r/2`-ball around it. -/
def cofinal_of_radius (r : ℝ) (rpos : r > 0) :
  { D : set (cniset α) // cofinal D } :=
{ val := { f | ∀ (x y ∈ f.val), dist x y ≤ r },
  property :=
    begin
      rintro ⟨C, hc, nic⟩,
      cases nic with x hx,
      refine ⟨⟨C ∩ closed_ball x (r/2), is_closed_inter hc is_closed_ball, _⟩, _, _⟩,
      { rw interior_inter,
        refine ⟨x, hx, _⟩,
        rw mem_interior,
        exact ⟨ball x (r/2), ball_subset_closed_ball, is_open_ball,
          mem_ball_self $ half_pos rpos⟩, },
      { rintros a b ⟨_, ha⟩ ⟨_, hb⟩,
        calc dist a b ≤ dist a x + dist b x : dist_triangle_right _ _ _
                  ... ≤ r/2 + r/2           : add_le_add ha hb
                  ... = r                   : add_halves r },
      apply inter_subset_left,
    end }

variables {ι : Type*} [encodable ι] (ℱ : ι → { s : set α // is_open s ∧ closure s = univ })

noncomputable def cofinal_family : ι ⊕ ℕ → { D : set (cniset α) // cofinal D }
| (sum.inl i) := cofinal_of_dense (ℱ i).val (ℱ i).property.1 (ℱ i).property.2
| (sum.inr n) := cofinal_of_radius (1 / (n+1)) nat.one_div_pos_of_nat

variable (st : cniset α)

def gencof : set (cniset α) := generic.cofilter st $ cofinal_family ℱ

def filt : filter α :=
{ sets := { x | ∃ y ∈ gencof ℱ st, subtype.val y ⊆ x },
  univ_sets := ⟨st, generic.starting_point_mem st _, subset_univ _⟩,
  sets_of_superset := λ x x' ⟨y, hy, hyx⟩ hs, ⟨y, hy, subset.trans hyx hs⟩,
  inter_sets :=
    begin
      rintros x x' ⟨y, hy, hyx⟩ ⟨y', hy', hyx'⟩,
      rcases generic.directed_on st (cofinal_family ℱ) y hy y' hy' with ⟨z, hz, hzy, hzy'⟩,
      refine ⟨z, hz, _⟩,
      calc z.val ⊆ y.val ∩ y'.val : subset_inter hzy hzy'
             ... ⊆ x     ∩ x'     : inter_subset_inter hyx hyx'
    end }

lemma filt.cauchy : cauchy (filt ℱ st) :=
begin
  rw metric.cauchy_iff,
  split,
  { suffices : ¬ ∅ ∈ filt ℱ st,
    { intro h,
      rw h at this,
      tauto, },
    rintros ⟨y, hy, h⟩,
    cases y.property.2 with w hw,
    exact h (interior_subset hw), },
  intros ε epos,
  cases exists_nat_one_div_lt epos with n nh,
  rcases generic.meets st (cofinal_family ℱ) (sum.inr n) with ⟨y, hy, hyn⟩,
  refine ⟨y.val, ⟨y, hy, subset.refl _⟩, _⟩,
  intros a b ha hb,
  calc dist a b ≤ 1 / (n+1) : hyn a b ha hb
            ... < ε         : nh
end

variable [complete_space α]

theorem baire' : (st.val ∩ ⋂ i, (ℱ i).val).nonempty :=
begin
  cases complete_space.complete (filt.cauchy ℱ st) with x hx,
  refine ⟨x, _, _⟩,
  { apply mem_of_closed_of_tendsto (filt.cauchy ℱ st).1 hx st.property.1,
    refine ⟨_, _, subset.refl _⟩,
    apply generic.starting_point_mem, },
  { rw mem_Inter,
    intro i,
    rcases generic.meets st (cofinal_family ℱ) (sum.inl i)
      with ⟨C, C_cf, hc⟩,
    apply hc,
    apply mem_of_closed_of_tendsto (filt.cauchy ℱ st).1 hx C.property.1,
    exact ⟨_, C_cf, subset.refl _⟩, },
end

I am curious about what people think of this style of proof! Do we have something like this in mathlib already?