Step
*
of Lemma
in-open-isect
∀[X:Type]. ∀[x:X]. ∀[A,B:Open(X)]. (x ∈ open-isect(A;B)
⇐⇒ x ∈ A ∧ x ∈ B)
BY
{ TACTIC:(Auto
THEN All (RepUR ``Open in-open open-isect``)
THEN Try ((RWO "sp-meet-is-top" (-1) THEN Auto))
THEN RWO "sp-meet-is-top" 0
THEN Auto) }
Latex:
Latex:
\mforall{}[X:Type]. \mforall{}[x:X]. \mforall{}[A,B:Open(X)]. (x \mmember{} open-isect(A;B) \mLeftarrow{}{}\mRightarrow{} x \mmember{} A \mwedge{} x \mmember{} B)
By
Latex:
TACTIC:(Auto
THEN All (RepUR ``Open in-open open-isect``)
THEN Try ((RWO "sp-meet-is-top" (-1) THEN Auto))
THEN RWO "sp-meet-is-top" 0
THEN Auto)
Home
Index