wip

Author: mkerjean

theories/normedtype_theory/tvs.v

@@ -573,9 +573,18 @@ HB.builders Context R E & Openat0_isConvexTvs R E.
 
 Local Notation open_from_openat0 := (open_from_openat0 R open_at0).
 
-#[local] Lemma opT : open_from_openat0 setT. Admitted.
+#[local] Lemma opT : open_from_openat0 setT.
+Proof.
+exists 0 => //; exists [set: E] => //=; first by exact: openat0T. 
+by apply/seteqP; split => x //= _; exists 0 => //; exists x; rewrite ?add0r.
+Qed.
 
-#[local]  Lemma opI : setI_closed open_from_openat0 . Admitted.
+#[local] Lemma opI : setI_closed open_from_openat0.
+Proof. 
+move=> /= A B; rewrite /open_from_openat0 /= => -[x [[A' Ao Ax]]] [y [[B' Bo By]]].
+exists (x + y) => //; exists (A' `&` B'); first by apply: open_atI.
+apply/seteqP; split => z /=.
+Admitted.
 
 #[local] Lemma op_bigU : forall (I : Type) (f : I -> set E), 
  (forall i, open_from_openat0 (f i)) -> open_from_openat0  (\bigcup_i f i). Admitted.