Add Trace_wFull.

6df34918 · François Clément · 2594c999 · 6df34918
Commit 6df34918 authored 2 years ago by François Clément
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_base.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_base.v
@@ -441,6 +441,11 @@ Proof.
 intros; unfold wEmpty; rewrite <- trace_emptyset_r; easy.
 Qed.

+Lemma Trace_wFull : wFull P -> wFull (Trace P V).
+Proof.
+intros; unfold wFull; rewrite <- trace_fullset_r; easy.
+Qed.
+
 Lemma Trace_Compl : Compl P -> Compl (Trace P V).
 Proof.
 intros HP A [B HB]; rewrite <- trace_compl; apply Tr; auto.