## Stream: general

### Topic: closure_compl_eq vs closure_compl

#### Kenny Lau (Oct 02 2018 at 19:30):

closure_compl_eq vs closure_compl

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

#### Kenny Lau (Oct 02 2018 at 19:31):

lemme blame this...

#### Kenny Lau (Oct 02 2018 at 19:32):

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

#### Patrick Massot (Oct 02 2018 at 19:32):

oh wow, there are actually adjacent!

#### Kenny Lau (Oct 02 2018 at 19:34):

actually, below and above these theorems:

#### Kenny Lau (Oct 02 2018 at 19:34):

@[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 (Oct 02 2018 at 19:34):

just like a sandwich

#### Kenny Lau (Oct 02 2018 at 20:28):

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

#### Kevin Buzzard (Oct 03 2018 at 07:17):

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

#### Patrick Massot (Oct 03 2018 at 07:20):

In principle this is very easy

Last updated: May 08 2021 at 04:14 UTC