Skip to content
Snippets Groups Projects
Commit 7034c92e authored by François Clément's avatar François Clément
Browse files

TODO: rename Subset.

parent 853f3603
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
+ 1
− 0
View file @ 7034c92e
......@@ -115,6 +115,7 @@ Section Trace_Def.
Context {U : Type}. (* Universe. *)
Variable A : set U.
(* TODO: find another name! *)
Inductive Subset : set_system U -> set_system U :=
| Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment