closure_compl_eq vs closure_compl

Stream: general

[Kenny Lau]

closure_compl_eq vs closure_compl

https://github.com/leanprover/mathlib/blob/master/analysis/topology/topological_space.lean#L261-L271

[Kenny Lau]

lemme blame this...

[Kenny Lau]

it's this change that moved the latter theorem from topology/topological_space.lean to analysis/topology/topological_space.lean

[Patrick Massot]

oh wow, there are actually adjacent!

[Kenny Lau]

actually, below and above these theorems:

[Kenny Lau]

@[simp] lemma interior_compl_eq {s : set α} : interior (- s) = - closure s :=
by simp [closure_eq_compl_interior_compl]

@[simp] lemma closure_compl_eq {s : set α} : closure (- s) = - interior s :=
by simp [closure_eq_compl_interior_compl]

lemma closure_compl {s : set α} : closure (-s) = - interior s :=
subset.antisymm
  (by simp [closure_subset_iff_subset_of_is_closed, compl_subset_compl, subset.refl])
  begin
    rw [compl_subset_comm, subset_interior_iff_subset_of_open, compl_subset_comm],
    exact subset_closure,
    exact is_open_compl_iff.mpr is_closed_closure
  end

lemma interior_compl {s : set α} : interior (-s) = - closure s :=
calc interior (- s) = - - interior (- s) : by simp
  ... = - closure (- (- s)) : by rw [closure_compl]
  ... = - closure s : by simp

[Kenny Lau]

just like a sandwich

[Johannes Hölzl]

gone https://github.com/leanprover/mathlib/commit/fff12f5889c7cd5a9169b42433eb14f3b53e7614

[Kenny Lau]

I'm quite surprised they have no dependencies...

[Kevin Buzzard]

I guess one could try and use meta magic to search for theorems with two distinct names?

[Patrick Massot]

In principle this is very easy