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

Make P an explicit argument.

parent 0a214db9
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
+ 2
− 2
View file @ e6e1b2d6
......@@ -108,8 +108,8 @@ 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.
Inductive Subset (P : set_system U) : set_system U :=
| Sub : forall B, P B -> incl B A -> Subset P B.
Definition Lift : subset_system A -> set_system U := liftp_any A.
Definition Lift_full : subset_system A -> set_system U :=
......
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