Zulip Chat Archive

Stream: general

Topic: is_open_{univ,empty}


Johan Commelin (Dec 04 2018 at 18:12):

Is there a reason for the following discrepancy?

#print is_open_univ
/- @[reducible]
def topological_space.is_open_univ : ∀ {α : Type u} (c : topological_space α), is_open c univ :=
λ (α : Type u) (c : topological_space α), [topological_space.is_open_univ c] -/
#print is_open_empty
/- @[simp]
theorem is_open_empty : ∀ {α : Type u} [_inst_1 : topological_space α], is_open ∅ :=
λ {α : Type u} [_inst_1 : topological_space α],
  eq.mpr (id (eq.rec (eq.refl (is_open ∅)) (eq.symm sUnion_empty))) (is_open_sUnion (λ (a : set α), false.elim)) -/

Reid Barton (Dec 04 2018 at 18:13):

You have the wrong is_open_univ I think

Reid Barton (Dec 04 2018 at 18:14):

You probably want the root namespace one

Johan Commelin (Dec 04 2018 at 18:14):

Aahrg, I see.

Johan Commelin (Dec 04 2018 at 18:15):

Otoh, because of proof irrelevance it doesn't really matter which one I'm using, I guess.

Reid Barton (Dec 04 2018 at 18:15):

I assumed you were concerned about the type: () vs []

Johan Commelin (Dec 04 2018 at 18:21):

Yes, I was.

Johan Commelin (Dec 04 2018 at 18:22):

There is all sorts of asymmetry. But using the _root_ version solves all my headaches (-;


Last updated: Dec 20 2023 at 11:08 UTC