Stream: math-comp analysis

Topic: eq_op to eq for classical_set ?

vlj (Aug 17 2021 at 18:48):

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: eqPtransform my goald to [disjoint closure A & B] == true and not to closure A & B = set0.

vlj (Aug 17 2021 at 18:52):

And rewrite /eqP doesn't transform anything at all

Pierre Roux (Aug 17 2021 at 19:53):

what about apply/set0P?

vlj (Aug 17 2021 at 20:06):

cannot apply view set0P

vlj (Aug 17 2021 at 20:06):

(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.
  ```

vlj (Aug 17 2021 at 20:08):

set0P is doing != and not `==

vlj (Aug 17 2021 at 22:06):

ho apply/eqP works !!

Last updated: Oct 13 2024 at 01:02 UTC