Zulip Chat Archive

Stream: general

Topic: closure_compl_eq vs closure_compl


view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:31):

lemme blame this...

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:32):

oh wow, there are actually adjacent!

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:34):

actually, below and above these theorems:

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 02 2018 at 19:34):

just like a sandwich

view this post on Zulip Johannes Hölzl (Oct 02 2018 at 20:27):

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

view this post on Zulip Kenny Lau (Oct 02 2018 at 20:28):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 03 2018 at 07:20):

In principle this is very easy


Last updated: May 08 2021 at 04:14 UTC