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

Add monotony of {Inter,Union}_any_closure.

parent 277490ed
No related branches found
No related tags found
Loading
......@@ -175,6 +175,20 @@ Section Any_Facts2.
Context {U : Type}.
Lemma Inter_any_closure_monot :
forall (P1 P2 : set_system U),
Incl P1 P2 -> Incl (Inter_any_closure P1) (Inter_any_closure P2).
Proof.
intros P1 P2 HP A [Q1 HQ1]; apply Iac, Incl_trans with P1; easy.
Qed.
Lemma Union_any_closure_monot :
forall (P1 P2 : set_system U),
Incl P1 P2 -> Incl (Union_any_closure P1) (Union_any_closure P2).
Proof.
intros P1 P2 HP A [Q1 HQ1]; apply Uac, Incl_trans with P1; easy.
Qed.
Lemma Inter_any_closure_complp_any_eq :
forall (P : set_system U),
Inter_any_closure (complp_any P) = complp_any (Union_any_closure P).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment