is_open_{univ,empty}

Stream: general

[Johan Commelin]

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]

You have the wrong is_open_univ I think

[Reid Barton]

You probably want the root namespace one

[Johan Commelin]

Aahrg, I see.

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

Yes, I was.

[Johan Commelin]

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