Hi,

I'd like to prove a lemma (`Lemma closureIOpen (A B: set T): open B -> [ disjoint A & B ] -> [ disjoint (closure A) & B].`

) but I'm having issue with the definition of `disjoint`

: is uses `== set0`

which means I can't use the other lemmas in the lib which use single equal equality.

I'm pretty sure there is a lemma to transform an `eq_op`

to `eq`

but I don't find it. For some reason `apply: eqP`

transform my goald to `[disjoint closure A & B] == true`

and not to `closure A & B = set0`

.

And `rewrite /eqP`

doesn't transform anything at all

what about `apply/set0P`

?

`cannot apply view set0P`

(for info the whole script is

```
From mathcomp Require Import classical_sets eqtype boolp seq order topology choice ssrfun.
Require Import ssreflect ssrbool.
Open Scope classical_set_scope.
Context {T: topologicalType}.
Implicit Types (A B : set T).
Lemma closureIOpen (A B: set T):
open B -> [ disjoint A & B ] -> [ disjoint (closure A) & B].
Proof.
move => openB disjointAB.
apply /set0P.
```
```

set0P is doing `!=`

and not `==

ho apply/eqP works !!

Last updated: Jun 25 2024 at 17:02 UTC