From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.finset.html | 1227 ++++++++++++++-------------
1 file changed, 615 insertions(+), 612 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.finset.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.finset.html b/docs/htmldoc/mathcomp.ssreflect.finset.html
index 9542bbf..b9f69c8 100644
--- a/docs/htmldoc/mathcomp.ssreflect.finset.html
+++ b/docs/htmldoc/mathcomp.ssreflect.finset.html
@@ -21,7 +21,6 @@
@@ -129,23 +128,23 @@
Variable T : finType.
-Inductive set_type : predArgType := FinSet of {ffun pred T}.
+Inductive set_type : predArgType := FinSet of {ffun pred T}.
Definition finfun_of_set A := let: FinSet f := A in f.
-Definition set_of of phant T := set_type.
+Definition set_of of phant T := set_type.
Identity Coercion type_of_set_of : set_of >-> set_type.
-Canonical set_subType := Eval hnf in [newType for finfun_of_set].
-Definition set_eqMixin := Eval hnf in [eqMixin of set_type by <:].
+Canonical set_subType := Eval hnf in [newType for finfun_of_set].
+Definition set_eqMixin := Eval hnf in [eqMixin of set_type by <:].
Canonical set_eqType := Eval hnf in EqType set_type set_eqMixin.
-Definition set_choiceMixin := [choiceMixin of set_type by <:].
+Definition set_choiceMixin := [choiceMixin of set_type by <:].
Canonical set_choiceType := Eval hnf in ChoiceType set_type set_choiceMixin.
-Definition set_countMixin := [countMixin of set_type by <:].
+Definition set_countMixin := [countMixin of set_type by <:].
Canonical set_countType := Eval hnf in CountType set_type set_countMixin.
-Canonical set_subCountType := Eval hnf in [subCountType of set_type].
-Definition set_finMixin := [finMixin of set_type by <:].
+Canonical set_subCountType := Eval hnf in [subCountType of set_type].
+Definition set_finMixin := [finMixin of set_type by <:].
Canonical set_finType := Eval hnf in FinType set_type set_finMixin.
-Canonical set_subFinType := Eval hnf in [subFinType of set_type].
+Canonical set_subFinType := Eval hnf in [subFinType of set_type].
End SetType.
@@ -155,7 +154,7 @@
Open Scope set_scope.
-Notation "{ 'set' T }" := (set_of (Phant T))
+Notation "{ 'set' T }" := (set_of (Phant T))
(at level 0, format "{ 'set' T }") : type_scope.
@@ -169,15 +168,15 @@
notation to make this technicality less obstrusive.
-
Notation "A :=: B" := (
A = B :> {set _})
+
Notation "A :=: B" := (
A = B :> {set _})
(
at level 70,
no associativity,
only parsing) :
set_scope.
-
Notation "A :<>: B" := (
A ≠ B :> {set _})
+
Notation "A :<>: B" := (
A ≠ B :> {set _})
(
at level 70,
no associativity,
only parsing) :
set_scope.
-
Notation "A :==: B" := (
A == B :> {set _})
+
Notation "A :==: B" := (
A == B :> {set _})
(
at level 70,
no associativity,
only parsing) :
set_scope.
-
Notation "A :!=: B" := (
A != B :> {set _})
+
Notation "A :!=: B" := (
A != B :> {set _})
(
at level 70,
no associativity,
only parsing) :
set_scope.
-
Notation "A :=P: B" := (
A =P B :> {set _})
+
Notation "A :=P: B" := (
A =P B :> {set _})
(
at level 70,
no associativity,
only parsing) :
set_scope.
@@ -186,8 +185,8 @@
Module Type SetDefSig.
-
Parameter finset :
∀ T :
finType,
pred T → {set T}.
-
Parameter pred_of_set :
∀ T,
set_type T → fin_pred_sort (
predPredType T).
+
Parameter finset :
∀ T :
finType,
pred T → {set T}.
+
Parameter pred_of_set :
∀ T,
set_type T → fin_pred_sort (
predPredType T).
@@ -197,45 +196,45 @@
coercion chaining code.
-
Axiom finsetE :
finset = finset_def.
-
Axiom pred_of_setE :
pred_of_set = pred_of_set_def.
+
Axiom finsetE :
finset = finset_def.
+
Axiom pred_of_setE :
pred_of_set = pred_of_set_def.
End SetDefSig.
Module SetDef :
SetDefSig.
Definition finset :=
finset_def.
Definition pred_of_set :=
pred_of_set_def.
-
Lemma finsetE :
finset = finset_def.
-
Lemma pred_of_setE :
pred_of_set = pred_of_set_def.
+
Lemma finsetE :
finset = finset_def.
+
Lemma pred_of_setE :
pred_of_set = pred_of_set_def.
End SetDef.
Notation finset :=
SetDef.finset.
Notation pred_of_set :=
SetDef.pred_of_set.
-
Canonical finset_unlock :=
Unlockable SetDef.finsetE.
-
Canonical pred_of_set_unlock :=
Unlockable SetDef.pred_of_setE.
+
Canonical finset_unlock :=
Unlockable SetDef.finsetE.
+
Canonical pred_of_set_unlock :=
Unlockable SetDef.pred_of_setE.
-
Notation "[ 'set' x : T | P ]" := (
finset (
fun x :
T ⇒
P%
B))
+
Notation "[ 'set' x : T | P ]" := (
finset (
fun x :
T ⇒
P%
B))
(
at level 0,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' x | P ]" :=
[set x : _ | P]
+
Notation "[ 'set' x | P ]" :=
[set x : _ | P]
(
at level 0,
x,
P at level 99,
format "[ 'set' x | P ]") :
set_scope.
-
Notation "[ 'set' x 'in' A ]" :=
[set x | x \in A]
+
Notation "[ 'set' x 'in' A ]" :=
[set x | x \in A]
(
at level 0,
x at level 99,
format "[ 'set' x 'in' A ]") :
set_scope.
-
Notation "[ 'set' x : T 'in' A ]" :=
[set x : T | x \in A]
+
Notation "[ 'set' x : T 'in' A ]" :=
[set x : T | x \in A]
(
at level 0,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' x : T | P & Q ]" :=
[set x : T | P && Q]
+
Notation "[ 'set' x : T | P & Q ]" :=
[set x : T | P && Q]
(
at level 0,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' x | P & Q ]" :=
[set x | P && Q ]
+
Notation "[ 'set' x | P & Q ]" :=
[set x | P && Q ]
(
at level 0,
x,
P at level 99,
format "[ 'set' x | P & Q ]") :
set_scope.
-
Notation "[ 'set' x : T 'in' A | P ]" :=
[set x : T | x \in A & P]
+
Notation "[ 'set' x : T 'in' A | P ]" :=
[set x : T | x \in A & P]
(
at level 0,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' x 'in' A | P ]" :=
[set x | x \in A & P]
+
Notation "[ 'set' x 'in' A | P ]" :=
[set x | x \in A & P]
(
at level 0,
x at level 99,
format "[ 'set' x 'in' A | P ]") :
set_scope.
-
Notation "[ 'set' x 'in' A | P & Q ]" :=
[set x in A | P && Q]
+
Notation "[ 'set' x 'in' A | P & Q ]" :=
[set x in A | P && Q]
(
at level 0,
x at level 99,
format "[ 'set' x 'in' A | P & Q ]") :
set_scope.
-
Notation "[ 'set' x : T 'in' A | P & Q ]" :=
[set x : T in A | P && Q]
+
Notation "[ 'set' x : T 'in' A | P & Q ]" :=
[set x : T in A | P && Q]
(
at level 0,
x at level 99,
only parsing) :
set_scope.
@@ -256,200 +255,202 @@
coercion to resolve mem A to @mem (predPredType T) (pred_of_set A).
This is left-associative due to historical limitations of the .. Notation.
@@ -459,94 +460,94 @@
associate on the left.
@@ -558,65 +559,65 @@
setIdP is a generalisation of setIP that applies to comprehensions.
@@ -627,28 +628,28 @@
@@ -659,46 +660,46 @@
@@ -709,67 +710,67 @@
@@ -780,19 +781,19 @@
@@ -803,67 +804,67 @@
@@ -874,155 +875,155 @@
-
Lemma subsetIl A B :
A :&: B \subset A.
+
Lemma subsetIl A B :
A :&: B \subset A.
-
Lemma subsetIr A B :
A :&: B \subset B.
+
Lemma subsetIr A B :
A :&: B \subset B.
-
Lemma subsetUl A B :
A \subset A :|: B.
+
Lemma subsetUl A B :
A \subset A :|: B.
-
Lemma subsetUr A B :
B \subset A :|: B.
+
Lemma subsetUr A B :
B \subset A :|: B.
-
Lemma subsetU1 x A :
A \subset x |: A.
+
Lemma subsetU1 x A :
A \subset x |: A.
-
Lemma subsetDl A B :
A :\: B \subset A.
+
Lemma subsetDl A B :
A :\: B \subset A.
-
Lemma subD1set A x :
A :\ x \subset A.
+
Lemma subD1set A x :
A :\ x \subset A.
-
Lemma subsetDr A B :
A :\: B \subset ~: B.
+
Lemma subsetDr A B :
A :\: B \subset ~: B.
-
Lemma sub1set A x :
([set x] \subset A) = (x \in A).
+
Lemma sub1set A x :
([set x] \subset A) = (x \in A).
-
Lemma cards1P A :
reflect (
∃ x, A = [set x]) (
#|A| == 1).
+
Lemma cards1P A :
reflect (
∃ x, A = [set x]) (
#|A| == 1).
-
Lemma subset1 A x :
(A \subset [set x]) = (A == [set x]) || (A == set0).
+
Lemma subset1 A x :
(A \subset [set x]) = (A == [set x]) || (A == set0).
-
Lemma powerset1 x :
powerset [set x] = [set set0; [set x]].
+
Lemma powerset1 x :
powerset [set x] = [set set0; [set x]].
-
Lemma setIidPl A B :
reflect (
A :&: B = A) (
A \subset B).
+
Lemma setIidPl A B :
reflect (
A :&: B = A) (
A \subset B).
-
Lemma setIidPr A B :
reflect (
A :&: B = B) (
B \subset A).
+
Lemma setIidPr A B :
reflect (
A :&: B = B) (
B \subset A).
-
Lemma cardsDS A B :
B \subset A → #|A :\: B| = (
#|A| - #|B|)%
N.
+
Lemma cardsDS A B :
B \subset A → #|A :\: B| = (
#|A| - #|B|)%
N.
-
Lemma setUidPl A B :
reflect (
A :|: B = A) (
B \subset A).
+
Lemma setUidPl A B :
reflect (
A :|: B = A) (
B \subset A).
-
Lemma setUidPr A B :
reflect (
A :|: B = B) (
A \subset B).
+
Lemma setUidPr A B :
reflect (
A :|: B = B) (
A \subset B).
-
Lemma setDidPl A B :
reflect (
A :\: B = A)
[disjoint A & B].
+
Lemma setDidPl A B :
reflect (
A :\: B = A)
[disjoint A & B].
-
Lemma subIset A B C :
(B \subset A) || (C \subset A) → (B :&: C \subset A).
+
Lemma subIset A B C :
(B \subset A) || (C \subset A) → (B :&: C \subset A).
-
Lemma subsetI A B C :
(A \subset B :&: C) = (A \subset B) && (A \subset C).
+
Lemma subsetI A B C :
(A \subset B :&: C) = (A \subset B) && (A \subset C).
-
Lemma subsetIP A B C :
reflect (
A \subset B ∧ A \subset C) (
A \subset B :&: C).
+
Lemma subsetIP A B C :
reflect (
A \subset B ∧ A \subset C) (
A \subset B :&: C).
-
Lemma subsetIidl A B :
(A \subset A :&: B) = (A \subset B).
+
Lemma subsetIidl A B :
(A \subset A :&: B) = (A \subset B).
-
Lemma subsetIidr A B :
(B \subset A :&: B) = (B \subset A).
+
Lemma subsetIidr A B :
(B \subset A :&: B) = (B \subset A).
-
Lemma powersetI A B :
powerset (
A :&: B)
= powerset A :&: powerset B.
+
Lemma powersetI A B :
powerset (
A :&: B)
= powerset A :&: powerset B.
-
Lemma subUset A B C :
(B :|: C \subset A) = (B \subset A) && (C \subset A).
+
Lemma subUset A B C :
(B :|: C \subset A) = (B \subset A) && (C \subset A).
-
Lemma subsetU A B C :
(A \subset B) || (A \subset C) → A \subset B :|: C.
+
Lemma subsetU A B C :
(A \subset B) || (A \subset C) → A \subset B :|: C.
-
Lemma subUsetP A B C :
reflect (
A \subset C ∧ B \subset C) (
A :|: B \subset C).
+
Lemma subUsetP A B C :
reflect (
A \subset C ∧ B \subset C) (
A :|: B \subset C).
-
Lemma subsetC A B :
(A \subset ~: B) = (B \subset ~: A).
+
Lemma subsetC A B :
(A \subset ~: B) = (B \subset ~: A).
-
Lemma subCset A B :
(~: A \subset B) = (~: B \subset A).
+
Lemma subCset A B :
(~: A \subset B) = (~: B \subset A).
-
Lemma subsetD A B C :
(A \subset B :\: C) = (A \subset B) && [disjoint A & C].
+
Lemma subsetD A B C :
(A \subset B :\: C) = (A \subset B) && [disjoint A & C].
-
Lemma subDset A B C :
(A :\: B \subset C) = (A \subset B :|: C).
+
Lemma subDset A B C :
(A :\: B \subset C) = (A \subset B :|: C).
Lemma subsetDP A B C :
-
reflect (
A \subset B ∧ [disjoint A & C]) (
A \subset B :\: C).
+
reflect (
A \subset B ∧ [disjoint A & C]) (
A \subset B :\: C).
-
Lemma setU_eq0 A B :
(A :|: B == set0) = (A == set0) && (B == set0).
+
Lemma setU_eq0 A B :
(A :|: B == set0) = (A == set0) && (B == set0).
-
Lemma setD_eq0 A B :
(A :\: B == set0) = (A \subset B).
+
Lemma setD_eq0 A B :
(A :\: B == set0) = (A \subset B).
-
Lemma setI_eq0 A B :
(A :&: B == set0) = [disjoint A & B].
+
Lemma setI_eq0 A B :
(A :&: B == set0) = [disjoint A & B].
-
Lemma disjoint_setI0 A B :
[disjoint A & B] → A :&: B = set0.
+
Lemma disjoint_setI0 A B :
[disjoint A & B] → A :&: B = set0.
-
Lemma subsetD1 A B x :
(A \subset B :\ x) = (A \subset B) && (x \notin A).
+
Lemma subsetD1 A B x :
(A \subset B :\ x) = (A \subset B) && (x \notin A).
-
Lemma subsetD1P A B x :
reflect (
A \subset B ∧ x \notin A) (
A \subset B :\ x).
+
Lemma subsetD1P A B x :
reflect (
A \subset B ∧ x \notin A) (
A \subset B :\ x).
-
Lemma properD1 A x :
x \in A → A :\ x \proper A.
+
Lemma properD1 A x :
x \in A → A :\ x \proper A.
-
Lemma properIr A B :
~~ (B \subset A) → A :&: B \proper B.
+
Lemma properIr A B :
~~ (B \subset A) → A :&: B \proper B.
-
Lemma properIl A B :
~~ (A \subset B) → A :&: B \proper A.
+
Lemma properIl A B :
~~ (A \subset B) → A :&: B \proper A.
-
Lemma properUr A B :
~~ (A \subset B) → B \proper A :|: B.
+
Lemma properUr A B :
~~ (A \subset B) → B \proper A :|: B.
-
Lemma properUl A B :
~~ (B \subset A) → A \proper A :|: B.
+
Lemma properUl A B :
~~ (B \subset A) → A \proper A :|: B.
-
Lemma proper1set A x :
([set x] \proper A) → (x \in A).
+
Lemma proper1set A x :
([set x] \proper A) → (x \in A).
-
Lemma properIset A B C :
(B \proper A) || (C \proper A) → (B :&: C \proper A).
+
Lemma properIset A B C :
(B \proper A) || (C \proper A) → (B :&: C \proper A).
-
Lemma properI A B C :
(A \proper B :&: C) → (A \proper B) && (A \proper C).
+
Lemma properI A B C :
(A \proper B :&: C) → (A \proper B) && (A \proper C).
-
Lemma properU A B C :
(B :|: C \proper A) → (B \proper A) && (C \proper A).
+
Lemma properU A B C :
(B :|: C \proper A) → (B \proper A) && (C \proper A).
-
Lemma properD A B C :
(A \proper B :\: C) → (A \proper B) && [disjoint A & C].
+
Lemma properD A B C :
(A \proper B :\: C) → (A \proper B) && [disjoint A & C].
End setOps.
-
Hint Resolve subsetT_hint.
+
Hint Resolve subsetT_hint :
core.
Section setOpsAlgebra.
@@ -1057,19 +1058,19 @@
Variables fT1 fT2 :
finType.
-
Variables (
A1 :
{set fT1}) (
A2 :
{set fT2}).
+
Variables (
A1 :
{set fT1}) (
A2 :
{set fT2}).
-
Definition setX :=
[set u | u.1 \in A1 & u.2 \in A2].
+
Definition setX :=
[set u | u.1 \in A1 & u.2 \in A2].
-
Lemma in_setX x1 x2 :
((x1, x2) \in setX) = (x1 \in A1) && (x2 \in A2).
+
Lemma in_setX x1 x2 :
((x1, x2) \in setX) = (x1 \in A1) && (x2 \in A2).
-
Lemma setXP x1 x2 :
reflect (
x1 \in A1 ∧ x2 \in A2) (
(x1, x2) \in setX).
+
Lemma setXP x1 x2 :
reflect (
x1 \in A1 ∧ x2 \in A2) (
(x1, x2) \in setX).
-
Lemma cardsX :
#|setX| = #|A1| × #|A2|.
+
Lemma cardsX :
#|setX| = #|A1| × #|A2|.
End CartesianProd.
@@ -1081,33 +1082,33 @@
Module Type ImsetSig.
Parameter imset :
∀ aT rT :
finType,
-
(aT → rT) → mem_pred aT → {set rT}.
+
(aT → rT) → mem_pred aT → {set rT}.
Parameter imset2 :
∀ aT1 aT2 rT :
finType,
-
(aT1 → aT2 → rT) → mem_pred aT1 → (aT1 → mem_pred aT2) → {set rT}.
-
Axiom imsetE :
imset = imset_def.
-
Axiom imset2E :
imset2 = imset2_def.
+
(aT1 → aT2 → rT) → mem_pred aT1 → (aT1 → mem_pred aT2) → {set rT}.
+
Axiom imsetE :
imset = imset_def.
+
Axiom imset2E :
imset2 = imset2_def.
End ImsetSig.
Module Imset :
ImsetSig.
Definition imset :=
imset_def.
Definition imset2 :=
imset2_def.
-
Lemma imsetE :
imset = imset_def.
-
Lemma imset2E :
imset2 = imset2_def.
+
Lemma imsetE :
imset = imset_def.
+
Lemma imset2E :
imset2 = imset2_def.
End Imset.
Notation imset :=
Imset.imset.
Notation imset2 :=
Imset.imset2.
-
Canonical imset_unlock :=
Unlockable Imset.imsetE.
-
Canonical imset2_unlock :=
Unlockable Imset.imset2E.
-
Definition preimset (
aT :
finType)
rT f (
R :
mem_pred rT) :=
-
[set x : aT | in_mem (
f x)
R].
+
Canonical imset_unlock :=
Unlockable Imset.imsetE.
+
Canonical imset2_unlock :=
Unlockable Imset.imset2E.
+
Definition preimset (
aT :
finType)
rT f (
R :
mem_pred rT) :=
+
[set x : aT | in_mem (
f x)
R].
-
Notation "f @^-1: A" := (
preimset f (
mem A)) (
at level 24) :
set_scope.
-
Notation "f @: A" := (
imset f (
mem A)) (
at level 24) :
set_scope.
-
Notation "f @2: ( A , B )" := (
imset2 f (
mem A) (
fun _ ⇒
mem B))
+
Notation "f @^-1: A" := (
preimset f (
mem A)) (
at level 24) :
set_scope.
+
Notation "f @: A" := (
imset f (
mem A)) (
at level 24) :
set_scope.
+
Notation "f @2: ( A , B )" := (
imset2 f (
mem A) (
fun _ ⇒
mem B))
(
at level 24,
format "f @2: ( A , B )") :
set_scope.
@@ -1117,19 +1118,19 @@
Comprehensions
-
Notation "[ 'set' E | x 'in' A ]" := (
(fun x ⇒
E) @: A)
+
Notation "[ 'set' E | x 'in' A ]" := (
(fun x ⇒
E) @: A)
(
at level 0,
E,
x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'") :
set_scope.
-
Notation "[ 'set' E | x 'in' A & P ]" :=
[set E | x in [set x in A | P]]
+
Notation "[ 'set' E | x 'in' A & P ]" :=
[set E | x in [set x in A | P]]
(
at level 0,
E,
x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A '/ ' & P ] ']'") :
set_scope.
-
Notation "[ 'set' E | x 'in' A , y 'in' B ]" :=
- (
imset2 (
fun x y ⇒
E) (
mem A) (
fun x ⇒ (
mem B)))
+
Notation "[ 'set' E | x 'in' A , y 'in' B ]" :=
+ (
imset2 (
fun x y ⇒
E) (
mem A) (
fun x ⇒ (
mem B)))
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x 'in' A , '/ ' y 'in' B ] ']'"
) :
set_scope.
-
Notation "[ 'set' E | x 'in' A , y 'in' B & P ]" :=
-
[set E | x in A, y in [set y in B | P]]
+
Notation "[ 'set' E | x 'in' A , y 'in' B & P ]" :=
+
[set E | x in A, y in [set y in B | P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x 'in' A , '/ ' y 'in' B '/ ' & P ] ']'"
) :
set_scope.
@@ -1141,16 +1142,16 @@
Typed variants.
-
Notation "[ 'set' E | x : T 'in' A ]" := (
(fun x :
T ⇒
E) @: A)
+
Notation "[ 'set' E | x : T 'in' A ]" := (
(fun x :
T ⇒
E) @: A)
(
at level 0,
E,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x : T 'in' A & P ]" :=
-
[set E | x : T in [set x : T in A | P]]
+
Notation "[ 'set' E | x : T 'in' A & P ]" :=
+
[set E | x : T in [set x : T in A | P]]
(
at level 0,
E,
x at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x : T 'in' A , y : U 'in' B ]" :=
- (
imset2 (
fun (
x :
T) (
y :
U) ⇒
E) (
mem A) (
fun (
x :
T) ⇒ (
mem B)))
+
Notation "[ 'set' E | x : T 'in' A , y : U 'in' B ]" :=
+ (
imset2 (
fun (
x :
T) (
y :
U) ⇒
E) (
mem A) (
fun (
x :
T) ⇒ (
mem B)))
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
-
[set E | x : T in A, y : U in [set y : U in B | P]]
+
Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
+
[set E | x : T in A, y : U in [set y : U in B | P]]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
@@ -1160,39 +1161,39 @@
Comprehensions over a type.
-
Notation "[ 'set' E | x : T ]" :=
[set E | x : T in predOfType T]
+
Notation "[ 'set' E | x : T ]" :=
[set E | x : T in predOfType T]
(
at level 0,
E,
x at level 99,
format "[ '[hv' 'set' E '/ ' | x : T ] ']'") :
set_scope.
-
Notation "[ 'set' E | x : T & P ]" :=
[set E | x : T in [set x : T | P]]
+
Notation "[ 'set' E | x : T & P ]" :=
[set E | x : T in [set x : T | P]]
(
at level 0,
E,
x at level 99,
format "[ '[hv' 'set' E '/ ' | x : T '/ ' & P ] ']'") :
set_scope.
-
Notation "[ 'set' E | x : T , y : U 'in' B ]" :=
-
[set E | x : T in predOfType T, y : U in B]
+
Notation "[ 'set' E | x : T , y : U 'in' B ]" :=
+
[set E | x : T in predOfType T, y : U in B]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U 'in' B ] ']'")
:
set_scope.
-
Notation "[ 'set' E | x : T , y : U 'in' B & P ]" :=
-
[set E | x : T, y : U in [set y in B | P]]
+
Notation "[ 'set' E | x : T , y : U 'in' B & P ]" :=
+
[set E | x : T, y : U in [set y in B | P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv ' 'set' E '/' | x : T , '/ ' y : U 'in' B '/' & P ] ']'"
) :
set_scope.
-
Notation "[ 'set' E | x : T 'in' A , y : U ]" :=
-
[set E | x : T in A, y : U in predOfType U]
+
Notation "[ 'set' E | x : T 'in' A , y : U ]" :=
+
[set E | x : T in A, y : U in predOfType U]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x : T 'in' A , '/ ' y : U ] ']'")
:
set_scope.
-
Notation "[ 'set' E | x : T 'in' A , y : U & P ]" :=
-
[set E | x : T in A, y : U in [set y in P]]
+
Notation "[ 'set' E | x : T 'in' A , y : U & P ]" :=
+
[set E | x : T in A, y : U in [set y in P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x : T 'in' A , '/ ' y : U & P ] ']'")
:
set_scope.
-
Notation "[ 'set' E | x : T , y : U ]" :=
-
[set E | x : T, y : U in predOfType U]
+
Notation "[ 'set' E | x : T , y : U ]" :=
+
[set E | x : T, y : U in predOfType U]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U ] ']'")
:
set_scope.
-
Notation "[ 'set' E | x : T , y : U & P ]" :=
-
[set E | x : T, y : U in [set y in P]]
+
Notation "[ 'set' E | x : T , y : U & P ]" :=
+
[set E | x : T, y : U in [set y in P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'set' E '/ ' | x : T , '/ ' y : U & P ] ']'")
:
set_scope.
@@ -1204,17 +1205,17 @@
Untyped variants.
-
Notation "[ 'set' E | x , y 'in' B ]" :=
[set E | x : _, y : _ in B]
+
Notation "[ 'set' E | x , y 'in' B ]" :=
[set E | x : _, y : _ in B]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x , y 'in' B & P ]" :=
[set E | x : _, y : _ in B & P]
+
Notation "[ 'set' E | x , y 'in' B & P ]" :=
[set E | x : _, y : _ in B & P]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x 'in' A , y ]" :=
[set E | x : _ in A, y : _]
+
Notation "[ 'set' E | x 'in' A , y ]" :=
[set E | x : _ in A, y : _]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x 'in' A , y & P ]" :=
[set E | x : _ in A, y : _ & P]
+
Notation "[ 'set' E | x 'in' A , y & P ]" :=
[set E | x : _ in A, y : _ & P]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x , y ]" :=
[set E | x : _, y : _]
+
Notation "[ 'set' E | x , y ]" :=
[set E | x : _, y : _]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
-
Notation "[ 'set' E | x , y & P ]" :=
[set E | x : _, y : _ & P ]
+
Notation "[ 'set' E | x , y & P ]" :=
[set E | x : _, y : _ & P ]
(
at level 0,
E,
x,
y at level 99,
only parsing) :
set_scope.
@@ -1224,43 +1225,43 @@
Print-only variants to work around the Coq pretty-printer K-term kink.
-
Notation "[ 'se' 't' E | x 'in' A , y 'in' B ]" :=
- (
imset2 (
fun x y ⇒
E) (
mem A) (
fun _ ⇒
mem B))
+
Notation "[ 'se' 't' E | x 'in' A , y 'in' B ]" :=
+ (
imset2 (
fun x y ⇒
E) (
mem A) (
fun _ ⇒
mem B))
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'se' 't' E '/ ' | x 'in' A , '/ ' y 'in' B ] ']'")
:
set_scope.
-
Notation "[ 'se' 't' E | x 'in' A , y 'in' B & P ]" :=
-
[se t E | x in A, y in [set y in B | P]]
+
Notation "[ 'se' 't' E | x 'in' A , y 'in' B & P ]" :=
+
[se t E | x in A, y in [set y in B | P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv ' 'se' 't' E '/' | x 'in' A , '/ ' y 'in' B '/' & P ] ']'"
) :
set_scope.
-
Notation "[ 'se' 't' E | x : T , y : U 'in' B ]" :=
- (
imset2 (
fun x (
y :
U) ⇒
E) (
mem (
predOfType T)) (
fun _ ⇒
mem B))
+
Notation "[ 'se' 't' E | x : T , y : U 'in' B ]" :=
+ (
imset2 (
fun x (
y :
U) ⇒
E) (
mem (
predOfType T)) (
fun _ ⇒
mem B))
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv ' 'se' 't' E '/' | x : T , '/ ' y : U 'in' B ] ']'")
:
set_scope.
-
Notation "[ 'se' 't' E | x : T , y : U 'in' B & P ]" :=
-
[se t E | x : T, y : U in [set y in B | P]]
+
Notation "[ 'se' 't' E | x : T , y : U 'in' B & P ]" :=
+
[se t E | x : T, y : U in [set y in B | P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv ' 'se' 't' E '/' | x : T , '/ ' y : U 'in' B '/' & P ] ']'"
) :
set_scope.
-
Notation "[ 'se' 't' E | x : T 'in' A , y : U ]" :=
- (
imset2 (
fun x y ⇒
E) (
mem A) (
fun _ :
T ⇒
mem (
predOfType U)))
+
Notation "[ 'se' 't' E | x : T 'in' A , y : U ]" :=
+ (
imset2 (
fun x y ⇒
E) (
mem A) (
fun _ :
T ⇒
mem (
predOfType U)))
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'se' 't' E '/ ' | x : T 'in' A , '/ ' y : U ] ']'")
:
set_scope.
-
Notation "[ 'se' 't' E | x : T 'in' A , y : U & P ]" :=
- (
imset2 (
fun x (
y :
U) ⇒
E) (
mem A) (
fun _ :
T ⇒
mem [set y \in P]))
+
Notation "[ 'se' 't' E | x : T 'in' A , y : U & P ]" :=
+ (
imset2 (
fun x (
y :
U) ⇒
E) (
mem A) (
fun _ :
T ⇒
mem [set y \in P]))
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv ' 'se' 't' E '/' | x : T 'in' A , '/ ' y : U '/' & P ] ']'"
) :
set_scope.
-
Notation "[ 'se' 't' E | x : T , y : U ]" :=
-
[se t E | x : T, y : U in predOfType U]
+
Notation "[ 'se' 't' E | x : T , y : U ]" :=
+
[se t E | x : T, y : U in predOfType U]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'se' 't' E '/ ' | x : T , '/ ' y : U ] ']'")
:
set_scope.
-
Notation "[ 'se' 't' E | x : T , y : U & P ]" :=
-
[se t E | x : T, y : U in [set y in P]]
+
Notation "[ 'se' 't' E | x : T , y : U & P ]" :=
+
[se t E | x : T, y : U in [set y in P]]
(
at level 0,
E,
x,
y at level 99,
format
"[ '[hv' 'se' 't' E '/' | x : T , '/ ' y : U '/' & P ] ']'")
:
set_scope.
@@ -1281,126 +1282,126 @@
Section ImsetProp.
-
Variables (
f :
aT → rT) (
f2 :
aT → aT2 → rT).
+
Variables (
f :
aT → rT) (
f2 :
aT → aT2 → rT).
-
Lemma imsetP D y :
reflect (
exists2 x, in_mem x D & y = f x) (
y \in imset f D).
+
Lemma imsetP D y :
reflect (
exists2 x, in_mem x D & y = f x) (
y \in imset f D).
-
CoInductive imset2_spec D1 D2 y :
Prop :=
-
Imset2spec x1 x2 of in_mem x1 D1 &
in_mem x2 (
D2 x1) &
y = f2 x1 x2.
+
Variant imset2_spec D1 D2 y :
Prop :=
+
Imset2spec x1 x2 of in_mem x1 D1 &
in_mem x2 (
D2 x1) &
y = f2 x1 x2.
-
Lemma imset2P D1 D2 y :
reflect (
imset2_spec D1 D2 y) (
y \in imset2 f2 D1 D2).
+
Lemma imset2P D1 D2 y :
reflect (
imset2_spec D1 D2 y) (
y \in imset2 f2 D1 D2).
-
Lemma mem_imset (
D :
pred aT)
x :
x \in D → f x \in f @: D.
+
Lemma mem_imset (
D :
{pred aT})
x :
x \in D → f x \in f @: D.
-
Lemma imset0 :
f @: set0 = set0.
+
Lemma imset0 :
f @: set0 = set0.
-
Lemma imset_eq0 (
A :
{set aT}) :
(f @: A == set0) = (A == set0).
+
Lemma imset_eq0 (
A :
{set aT}) :
(f @: A == set0) = (A == set0).
-
Lemma imset_set1 x :
f @: [set x] = [set f x].
+
Lemma imset_set1 x :
f @: [set x] = [set f x].
-
Lemma mem_imset2 (
D :
pred aT) (
D2 :
aT → pred aT2)
x x2 :
-
x \in D → x2 \in D2 x →
-
f2 x x2 \in imset2 f2 (
mem D) (
fun x1 ⇒
mem (
D2 x1)).
+
Lemma mem_imset2 (
D :
{pred aT}) (
D2 :
aT → {pred aT2})
x x2 :
+
x \in D → x2 \in D2 x →
+
f2 x x2 \in imset2 f2 (
mem D) (
fun x1 ⇒
mem (
D2 x1)).
-
Lemma sub_imset_pre (
A :
pred aT) (
B :
pred rT) :
-
(f @: A \subset B) = (A \subset f @^-1: B).
+
Lemma sub_imset_pre (
A :
{pred aT}) (
B :
{pred rT}) :
+
(f @: A \subset B) = (A \subset f @^-1: B).
-
Lemma preimsetS (
A B :
pred rT) :
-
A \subset B → (f @^-1: A) \subset (f @^-1: B).
+
Lemma preimsetS (
A B :
{pred rT}) :
+
A \subset B → (f @^-1: A) \subset (f @^-1: B).
-
Lemma preimset0 :
f @^-1: set0 = set0.
+
Lemma preimset0 :
f @^-1: set0 = set0.
-
Lemma preimsetT :
f @^-1: setT = setT.
+
Lemma preimsetT :
f @^-1: setT = setT.
-
Lemma preimsetI (
A B :
{set rT}) :
-
f @^-1: (A :&: B) = (f @^-1: A) :&: (f @^-1: B).
+
Lemma preimsetI (
A B :
{set rT}) :
+
f @^-1: (A :&: B) = (f @^-1: A) :&: (f @^-1: B).
-
Lemma preimsetU (
A B :
{set rT}) :
-
f @^-1: (A :|: B) = (f @^-1: A) :|: (f @^-1: B).
+
Lemma preimsetU (
A B :
{set rT}) :
+
f @^-1: (A :|: B) = (f @^-1: A) :|: (f @^-1: B).
-
Lemma preimsetD (
A B :
{set rT}) :
-
f @^-1: (A :\: B) = (f @^-1: A) :\: (f @^-1: B).
+
Lemma preimsetD (
A B :
{set rT}) :
+
f @^-1: (A :\: B) = (f @^-1: A) :\: (f @^-1: B).
-
Lemma preimsetC (
A :
{set rT}) :
f @^-1: (~: A) = ~: f @^-1: A.
+
Lemma preimsetC (
A :
{set rT}) :
f @^-1: (~: A) = ~: f @^-1: A.
-
Lemma imsetS (
A B :
pred aT) :
A \subset B → f @: A \subset f @: B.
+
Lemma imsetS (
A B :
{pred aT}) :
A \subset B → f @: A \subset f @: B.
-
Lemma imset_proper (
A B :
{set aT}) :
-
{in B &, injective f} → A \proper B → f @: A \proper f @: B.
+
Lemma imset_proper (
A B :
{set aT}) :
+
{in B &, injective f} → A \proper B → f @: A \proper f @: B.
-
Lemma preimset_proper (
A B :
{set rT}) :
-
B \subset codom f → A \proper B → (f @^-1: A) \proper (f @^-1: B).
+
Lemma preimset_proper (
A B :
{set rT}) :
+
B \subset codom f → A \proper B → (f @^-1: A) \proper (f @^-1: B).
-
Lemma imsetU (
A B :
{set aT}) :
f @: (A :|: B) = (f @: A) :|: (f @: B).
+
Lemma imsetU (
A B :
{set aT}) :
f @: (A :|: B) = (f @: A) :|: (f @: B).
-
Lemma imsetU1 a (
A :
{set aT}) :
f @: (a |: A) = f a |: (f @: A).
+
Lemma imsetU1 a (
A :
{set aT}) :
f @: (a |: A) = f a |: (f @: A).
-
Lemma imsetI (
A B :
{set aT}) :
-
{in A & B, injective f} → f @: (A :&: B) = f @: A :&: f @: B.
+
Lemma imsetI (
A B :
{set aT}) :
+
{in A & B, injective f} → f @: (A :&: B) = f @: A :&: f @: B.
-
Lemma imset2Sl (
A B :
pred aT) (
C :
pred aT2) :
-
A \subset B → f2 @2: (A, C) \subset f2 @2: (B, C).
+
Lemma imset2Sl (
A B :
{pred aT}) (
C :
{pred aT2}) :
+
A \subset B → f2 @2: (A, C) \subset f2 @2: (B, C).
-
Lemma imset2Sr (
A B :
pred aT2) (
C :
pred aT) :
-
A \subset B → f2 @2: (C, A) \subset f2 @2: (C, B).
+
Lemma imset2Sr (
A B :
{pred aT2}) (
C :
{pred aT}) :
+
A \subset B → f2 @2: (C, A) \subset f2 @2: (C, B).
-
Lemma imset2S (
A B :
pred aT) (
A2 B2 :
pred aT2) :
-
A \subset B → A2 \subset B2 → f2 @2: (A, A2) \subset f2 @2: (B, B2).
+
Lemma imset2S (
A B :
{pred aT}) (
A2 B2 :
{pred aT2}) :
+
A \subset B → A2 \subset B2 → f2 @2: (A, A2) \subset f2 @2: (B, B2).
End ImsetProp.
-
Implicit Types (
f g :
aT → rT) (
D :
{set aT}) (
R :
pred rT).
+
Implicit Types (
f g :
aT → rT) (
D :
{set aT}) (
R :
{pred rT}).
-
Lemma eq_preimset f g R :
f =1 g → f @^-1: R = g @^-1: R.
+
Lemma eq_preimset f g R :
f =1 g → f @^-1: R = g @^-1: R.
-
Lemma eq_imset f g D :
f =1 g → f @: D = g @: D.
+
Lemma eq_imset f g D :
f =1 g → f @: D = g @: D.
-
Lemma eq_in_imset f g D :
{in D, f =1 g} → f @: D = g @: D.
+
Lemma eq_in_imset f g D :
{in D, f =1 g} → f @: D = g @: D.
-
Lemma eq_in_imset2 (
f g :
aT → aT2 → rT) (
D :
pred aT) (
D2 :
pred aT2) :
-
{in D & D2, f =2 g} → f @2: (D, D2) = g @2: (D, D2).
+
Lemma eq_in_imset2 (
f g :
aT → aT2 → rT) (
D :
{pred aT}) (
D2 :
{pred aT2}) :
+
{in D & D2, f =2 g} → f @2: (D, D2) = g @2: (D, D2).
End ImsetTheory.
-
Lemma imset2_pair (
A :
{set aT}) (
B :
{set aT2}) :
-
[set (x, y) | x in A, y in B] = setX A B.
+
Lemma imset2_pair (
A :
{set aT}) (
B :
{set aT2}) :
+
[set (x, y) | x in A, y in B] = setX A B.
-
Lemma setXS (
A1 B1 :
{set aT}) (
A2 B2 :
{set aT2}) :
-
A1 \subset B1 → A2 \subset B2 → setX A1 A2 \subset setX B1 B2.
+
Lemma setXS (
A1 B1 :
{set aT}) (
A2 B2 :
{set aT2}) :
+
A1 \subset B1 → A2 \subset B2 → setX A1 A2 \subset setX B1 B2.
End FunImage.
@@ -1414,46 +1415,50 @@
Variables (
R :
Type) (
idx :
R).
Variables (
op :
Monoid.law idx) (
aop :
Monoid.com_law idx).
Variables I J :
finType.
-
Implicit Type A B :
{set I}.
-
Implicit Type h :
I → J.
-
Implicit Type P :
pred I.
-
Implicit Type F :
I → R.
+
Implicit Type A B :
{set I}.
+
Implicit Type h :
I → J.
+
Implicit Type P :
pred I.
+
Implicit Type F :
I → R.
-
Lemma big_set0 F :
\big[op/idx]_(i in set0) F i = idx.
+
Lemma big_set0 F :
\big[op/idx]_(i in set0) F i = idx.
-
Lemma big_set1 a F :
\big[op/idx]_(i in [set a]) F i = F a.
+
Lemma big_set1 a F :
\big[op/idx]_(i in [set a]) F i = F a.
-
-
Lemma big_setIDdep A B P F :
-
\big[aop/idx]_(i in A | P i) F i =
-
aop (
\big[aop/idx]_(i in A :&: B | P i) F i)
- (
\big[aop/idx]_(i in A :\: B | P i) F i).
-
Lemma big_setID A B F :
-
\big[aop/idx]_(i in A) F i =
-
aop (
\big[aop/idx]_(i in A :&: B) F i)
- (
\big[aop/idx]_(i in A :\: B) F i).
+
\big[aop/idx]_(i in A) F i =
+
aop (
\big[aop/idx]_(i in A :&: B) F i)
+ (
\big[aop/idx]_(i in A :\: B) F i).
-
Lemma big_setD1 a A F :
a \in A →
-
\big[aop/idx]_(i in A) F i = aop (
F a) (
\big[aop/idx]_(i in A :\ a) F i).
+
Lemma big_setIDcond A B P F :
+
\big[aop/idx]_(i in A | P i) F i =
+
aop (
\big[aop/idx]_(i in A :&: B | P i) F i)
+ (
\big[aop/idx]_(i in A :\: B | P i) F i).
+
+
+
Lemma big_setD1 a A F :
a \in A →
+
\big[aop/idx]_(i in A) F i = aop (
F a) (
\big[aop/idx]_(i in A :\ a) F i).
-
Lemma big_setU1 a A F :
a \notin A →
-
\big[aop/idx]_(i in a |: A) F i = aop (
F a) (
\big[aop/idx]_(i in A) F i).
+
Lemma big_setU1 a A F :
a \notin A →
+
\big[aop/idx]_(i in a |: A) F i = aop (
F a) (
\big[aop/idx]_(i in A) F i).
-
Lemma big_imset h (
A :
pred I)
G :
-
{in A &, injective h} →
-
\big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (
h i).
+
Lemma big_imset h (
A :
{pred I})
G :
{in A &, injective h} →
+
\big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (
h i).
-
Lemma partition_big_imset h (
A :
pred I)
F :
-
\big[aop/idx]_(i in A) F i =
-
\big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.
+
Lemma big_imset_cond h (
A :
{pred I}) (
P :
pred J)
G :
{in A &, injective h} →
+
\big[aop/idx]_(j in h @: A | P j) G j =
+
\big[aop/idx]_(i in A | P (
h i)
) G (
h i).
+
+
+
Lemma partition_big_imset h (
A :
{pred I})
F :
+
\big[aop/idx]_(i in A) F i =
+
\big[aop/idx]_(j in h @: A) \big[aop/idx]_(i in A | h i == j) F i.
End BigOps.
@@ -1465,13 +1470,13 @@
Variables aT1 aT2 rT :
finType.
-
Variables (
f :
aT1 → aT2 → rT).
+
Variables (
f :
aT1 → aT2 → rT).
-
Lemma imset2_set1l x1 (
D2 :
pred aT2) :
f @2: ([set x1], D2) = f x1 @: D2.
+
Lemma imset2_set1l x1 (
D2 :
{pred aT2}) :
f @2: ([set x1], D2) = f x1 @: D2.
-
Lemma imset2_set1r x2 (
D1 :
pred aT1) :
f @2: (D1, [set x2]) = f^~ x2 @: D1.
+
Lemma imset2_set1r x2 (
D1 :
{pred aT1}) :
f @2: (D1, [set x2]) = f^~ x2 @: D1.
End Fun2Set1.
@@ -1481,30 +1486,30 @@
Variables aT aT2 rT :
finType.
-
Variables (
f :
aT → rT) (
g :
rT → aT) (
f2 :
aT → aT2 → rT).
-
Variables (
D :
pred aT) (
D2 :
pred aT).
+
Variables (
f :
aT → rT) (
g :
rT → aT) (
f2 :
aT → aT2 → rT).
+
Variables (
D :
{pred aT}) (
D2 :
{pred aT}).
-
Lemma imset_card :
#|f @: D| = #|image f D|.
+
Lemma imset_card :
#|f @: D| = #|image f D|.
-
Lemma leq_imset_card :
#|f @: D| ≤ #|D|.
+
Lemma leq_imset_card :
#|f @: D| ≤ #|D|.
-
Lemma card_in_imset :
{in D &, injective f} → #|f @: D| = #|D|.
+
Lemma card_in_imset :
{in D &, injective f} → #|f @: D| = #|D|.
-
Lemma card_imset :
injective f → #|f @: D| = #|D|.
+
Lemma card_imset :
injective f → #|f @: D| = #|D|.
-
Lemma imset_injP :
reflect {in D &, injective f} (
#|f @: D| == #|D|).
+
Lemma imset_injP :
reflect {in D &, injective f} (
#|f @: D| == #|D|).
Lemma can2_in_imset_pre :
-
{in D, cancel f g} → {on D, cancel g & f} → f @: D = g @^-1: D.
+
{in D, cancel f g} → {on D, cancel g & f} → f @: D = g @^-1: D.
-
Lemma can2_imset_pre :
cancel f g → cancel g f → f @: D = g @^-1: D.
+
Lemma can2_imset_pre :
cancel f g → cancel g f → f @: D = g @^-1: D.
End CardFunImage.
@@ -1512,22 +1517,22 @@
-
Lemma on_card_preimset (
aT rT :
finType) (
f :
aT → rT) (
R :
pred rT) :
-
{on R, bijective f} → #|f @^-1: R| = #|R|.
+
Lemma on_card_preimset (
aT rT :
finType) (
f :
aT → rT) (
R :
{pred rT}) :
+
{on R, bijective f} → #|f @^-1: R| = #|R|.
-
Lemma can_imset_pre (
T :
finType)
f g (
A :
{set T}) :
-
cancel f g → f @: A = g @^-1: A :> {set T}.
+
Lemma can_imset_pre (
T :
finType)
f g (
A :
{set T}) :
+
cancel f g → f @: A = g @^-1: A :> {set T}.
-
Lemma imset_id (
T :
finType) (
A :
{set T}) :
[set x | x in A] = A.
+
Lemma imset_id (
T :
finType) (
A :
{set T}) :
[set x | x in A] = A.
-
Lemma card_preimset (
T :
finType) (
f :
T → T) (
A :
{set T}) :
-
injective f → #|f @^-1: A| = #|A|.
+
Lemma card_preimset (
T :
finType) (
f :
T → T) (
A :
{set T}) :
+
injective f → #|f @^-1: A| = #|A|.
-
Lemma card_powerset (
T :
finType) (
A :
{set T}) :
#|powerset A| = 2
^ #|A|.
+
Lemma card_powerset (
T :
finType) (
A :
{set T}) :
#|powerset A| = 2
^ #|A|.
Section FunImageComp.
@@ -1536,70 +1541,70 @@
Variables T T' U :
finType.
-
Lemma imset_comp (
f :
T' → U) (
g :
T → T') (
H :
pred T) :
-
(f \o g) @: H = f @: (g @: H).
+
Lemma imset_comp (
f :
T' → U) (
g :
T → T') (
H :
{pred T}) :
+
(f \o g) @: H = f @: (g @: H).
End FunImageComp.
-
Notation "\bigcup_ ( i <- r | P ) F" :=
- (
\big[@
setU _/set0]_(i <- r | P) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i <- r ) F" :=
- (
\big[@
setU _/set0]_(i <- r) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( m <= i < n | P ) F" :=
- (
\big[@
setU _/set0]_(m ≤ i < n | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( m <= i < n ) F" :=
- (
\big[@
setU _/set0]_(m ≤ i < n) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i | P ) F" :=
- (
\big[@
setU _/set0]_(i | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcup_ i F" :=
- (
\big[@
setU _/set0]_i F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i : t | P ) F" :=
- (
\big[@
setU _/set0]_(i : t | P%
B) F%
SET) (
only parsing):
set_scope.
-
Notation "\bigcup_ ( i : t ) F" :=
- (
\big[@
setU _/set0]_(i : t) F%
SET) (
only parsing) :
set_scope.
-
Notation "\bigcup_ ( i < n | P ) F" :=
- (
\big[@
setU _/set0]_(i < n | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i < n ) F" :=
- (
\big[@
setU _/set0]_ (i < n) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i 'in' A | P ) F" :=
- (
\big[@
setU _/set0]_(i in A | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcup_ ( i 'in' A ) F" :=
- (
\big[@
setU _/set0]_(i in A) F%
SET) :
set_scope.
-
-
-
Notation "\bigcap_ ( i <- r | P ) F" :=
- (
\big[@
setI _/setT]_(i <- r | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i <- r ) F" :=
- (
\big[@
setI _/setT]_(i <- r) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( m <= i < n | P ) F" :=
- (
\big[@
setI _/setT]_(m ≤ i < n | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( m <= i < n ) F" :=
- (
\big[@
setI _/setT]_(m ≤ i < n) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i | P ) F" :=
- (
\big[@
setI _/setT]_(i | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcap_ i F" :=
- (
\big[@
setI _/setT]_i F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i : t | P ) F" :=
- (
\big[@
setI _/setT]_(i : t | P%
B) F%
SET) (
only parsing):
set_scope.
-
Notation "\bigcap_ ( i : t ) F" :=
- (
\big[@
setI _/setT]_(i : t) F%
SET) (
only parsing) :
set_scope.
-
Notation "\bigcap_ ( i < n | P ) F" :=
- (
\big[@
setI _/setT]_(i < n | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i < n ) F" :=
- (
\big[@
setI _/setT]_(i < n) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i 'in' A | P ) F" :=
- (
\big[@
setI _/setT]_(i in A | P%
B) F%
SET) :
set_scope.
-
Notation "\bigcap_ ( i 'in' A ) F" :=
- (
\big[@
setI _/setT]_(i in A) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i <- r | P ) F" :=
+ (
\big[@
setU _/set0]_(i <- r | P) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i <- r ) F" :=
+ (
\big[@
setU _/set0]_(i <- r) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( m <= i < n | P ) F" :=
+ (
\big[@
setU _/set0]_(m ≤ i < n | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( m <= i < n ) F" :=
+ (
\big[@
setU _/set0]_(m ≤ i < n) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i | P ) F" :=
+ (
\big[@
setU _/set0]_(i | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcup_ i F" :=
+ (
\big[@
setU _/set0]_i F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i : t | P ) F" :=
+ (
\big[@
setU _/set0]_(i : t | P%
B) F%
SET) (
only parsing):
set_scope.
+
Notation "\bigcup_ ( i : t ) F" :=
+ (
\big[@
setU _/set0]_(i : t) F%
SET) (
only parsing) :
set_scope.
+
Notation "\bigcup_ ( i < n | P ) F" :=
+ (
\big[@
setU _/set0]_(i < n | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i < n ) F" :=
+ (
\big[@
setU _/set0]_ (i < n) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i 'in' A | P ) F" :=
+ (
\big[@
setU _/set0]_(i in A | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcup_ ( i 'in' A ) F" :=
+ (
\big[@
setU _/set0]_(i in A) F%
SET) :
set_scope.
+
+
+
Notation "\bigcap_ ( i <- r | P ) F" :=
+ (
\big[@
setI _/setT]_(i <- r | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i <- r ) F" :=
+ (
\big[@
setI _/setT]_(i <- r) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( m <= i < n | P ) F" :=
+ (
\big[@
setI _/setT]_(m ≤ i < n | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( m <= i < n ) F" :=
+ (
\big[@
setI _/setT]_(m ≤ i < n) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i | P ) F" :=
+ (
\big[@
setI _/setT]_(i | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcap_ i F" :=
+ (
\big[@
setI _/setT]_i F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i : t | P ) F" :=
+ (
\big[@
setI _/setT]_(i : t | P%
B) F%
SET) (
only parsing):
set_scope.
+
Notation "\bigcap_ ( i : t ) F" :=
+ (
\big[@
setI _/setT]_(i : t) F%
SET) (
only parsing) :
set_scope.
+
Notation "\bigcap_ ( i < n | P ) F" :=
+ (
\big[@
setI _/setT]_(i < n | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i < n ) F" :=
+ (
\big[@
setI _/setT]_(i < n) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i 'in' A | P ) F" :=
+ (
\big[@
setI _/setT]_(i in A | P%
B) F%
SET) :
set_scope.
+
Notation "\bigcap_ ( i 'in' A ) F" :=
+ (
\big[@
setI _/setT]_(i in A) F%
SET) :
set_scope.
Section BigSetOps.
Variables T I :
finType.
-
Implicit Types (
U :
pred T) (
P :
pred I) (
A B :
{set I}) (
F :
I → {set T}).
+
Implicit Types (
U :
{pred T}) (
P :
pred I) (
A B :
{set I}) (
F :
I → {set T}).
-
Lemma bigcap_inf j P F :
P j → \bigcap_(i | P i) F i \subset F j.
+
Lemma bigcap_inf j P F :
P j → \bigcap_(i | P i) F i \subset F j.
Lemma bigcap_min j U P F :
-
P j → F j \subset U → \bigcap_(i | P i) F i \subset U.
+
P j → F j \subset U → \bigcap_(i | P i) F i \subset U.
Lemma bigcapsP U P F :
-
reflect (
∀ i,
P i → U \subset F i) (
U \subset \bigcap_(i | P i) F i).
+
reflect (
∀ i,
P i → U \subset F i) (
U \subset \bigcap_(i | P i) F i).
Lemma bigcapP x P F :
-
reflect (
∀ i,
P i → x \in F i) (
x \in \bigcap_(i | P i) F i).
+
reflect (
∀ i,
P i → x \in F i) (
x \in \bigcap_(i | P i) F i).
-
Lemma setC_bigcup J r (
P :
pred J) (
F :
J → {set T}) :
-
~: (\bigcup_(j <- r | P j) F j) = \bigcap_(j <- r | P j) ~: F j.
+
Lemma setC_bigcup J r (
P :
pred J) (
F :
J → {set T}) :
+
~: (\bigcup_(j <- r | P j) F j) = \bigcap_(j <- r | P j) ~: F j.
-
Lemma setC_bigcap J r (
P :
pred J) (
F :
J → {set T}) :
-
~: (\bigcap_(j <- r | P j) F j) = \bigcup_(j <- r | P j) ~: F j.
+
Lemma setC_bigcap J r (
P :
pred J) (
F :
J → {set T}) :
+
~: (\bigcap_(j <- r | P j) F j) = \bigcup_(j <- r | P j) ~: F j.
Lemma bigcap_setU A B F :
-
(\bigcap_(i in A :|: B) F i) =
-
(\bigcap_(i in A) F i) :&: (\bigcap_(i in B) F i).
+
(\bigcap_(i in A :|: B) F i) =
+
(\bigcap_(i in A) F i) :&: (\bigcap_(i in B) F i).
-
Lemma bigcap_seq r F :
\bigcap_(i <- r) F i = \bigcap_(i in r) F i.
+
Lemma bigcap_seq r F :
\bigcap_(i <- r) F i = \bigcap_(i in r) F i.
End BigSetOps.
@@ -1681,34 +1686,34 @@
Section ImsetCurry.
-
Variables (
aT1 aT2 rT :
finType) (
f :
aT1 → aT2 → rT).
+
Variables (
aT1 aT2 rT :
finType) (
f :
aT1 → aT2 → rT).
Section Curry.
-
Variables (
A1 :
{set aT1}) (
A2 :
{set aT2}).
-
Variables (
D1 :
pred aT1) (
D2 :
pred aT2).
+
Variables (
A1 :
{set aT1}) (
A2 :
{set aT2}).
+
Variables (
D1 :
{pred aT1}) (
D2 :
{pred aT2}).
-
Lemma curry_imset2X :
f @2: (A1, A2) = prod_curry f @: (setX A1 A2).
+
Lemma curry_imset2X :
f @2: (A1, A2) = prod_curry f @: (setX A1 A2).
-
Lemma curry_imset2l :
f @2: (D1, D2) = \bigcup_(x1 in D1) f x1 @: D2.
+
Lemma curry_imset2l :
f @2: (D1, D2) = \bigcup_(x1 in D1) f x1 @: D2.
-
Lemma curry_imset2r :
f @2: (D1, D2) = \bigcup_(x2 in D2) f^~ x2 @: D1.
+
Lemma curry_imset2r :
f @2: (D1, D2) = \bigcup_(x2 in D2) f^~ x2 @: D1.
End Curry.
-
Lemma imset2Ul (
A B :
{set aT1}) (
C :
{set aT2}) :
-
f @2: (A :|: B, C) = f @2: (A, C) :|: f @2: (B, C).
+
Lemma imset2Ul (
A B :
{set aT1}) (
C :
{set aT2}) :
+
f @2: (A :|: B, C) = f @2: (A, C) :|: f @2: (B, C).
-
Lemma imset2Ur (
A :
{set aT1}) (
B C :
{set aT2}) :
-
f @2: (A, B :|: C) = f @2: (A, B) :|: f @2: (A, C).
+
Lemma imset2Ur (
A :
{set aT1}) (
B C :
{set aT2}) :
+
f @2: (A, B :|: C) = f @2: (A, B) :|: f @2: (A, C).
End ImsetCurry.
@@ -1718,110 +1723,110 @@
Variables T I :
finType.
-
Implicit Types (
x y z :
T) (
A B D X :
{set T}) (
P Q :
{set {set T}}).
-
Implicit Types (
J :
pred I) (
F :
I → {set T}).
+
Implicit Types (
x y z :
T) (
A B D X :
{set T}) (
P Q :
{set {set T}}).
+
Implicit Types (
J :
pred I) (
F :
I → {set T}).
-
Definition cover P :=
\bigcup_(B in P) B.
-
Definition pblock P x :=
odflt set0 (
pick [pred B in P | x \in B]).
-
Definition trivIset P :=
\sum_(B in P) #|B| == #|cover P|.
-
Definition partition P D :=
[&& cover P == D, trivIset P & set0 \notin P].
+
Definition cover P :=
\bigcup_(B in P) B.
+
Definition pblock P x :=
odflt set0 (
pick [pred B in P | x \in B]).
+
Definition trivIset P :=
\sum_(B in P) #|B| == #|cover P|.
+
Definition partition P D :=
[&& cover P == D, trivIset P & set0 \notin P].
Definition is_transversal X P D :=
-
[&& partition P D, X \subset D & [∀ B in P, #|X :&: B| == 1
]].
-
Definition transversal P D :=
[set odflt x [pick y in pblock P x] | x in D].
-
Definition transversal_repr x0 X B :=
odflt x0 [pick x in X :&: B].
+
[&& partition P D, X \subset D & [∀ B in P, #|X :&: B| == 1
]].
+
Definition transversal P D :=
[set odflt x [pick y in pblock P x] | x in D].
+
Definition transversal_repr x0 X B :=
odflt x0 [pick x in X :&: B].
-
Lemma leq_card_setU A B :
#|A :|: B| ≤ #|A| + #|B| ?= iff [disjoint A & B].
+
Lemma leq_card_setU A B :
#|A :|: B| ≤ #|A| + #|B| ?= iff [disjoint A & B].
-
Lemma leq_card_cover P :
#|cover P| ≤ \sum_(A in P) #|A| ?= iff trivIset P.
+
Lemma leq_card_cover P :
#|cover P| ≤ \sum_(A in P) #|A| ?= iff trivIset P.
Lemma trivIsetP P :
-
reflect {in P &, ∀ A B,
A != B → [disjoint A & B]} (
trivIset P).
+
reflect {in P &, ∀ A B,
A != B → [disjoint A & B]} (
trivIset P).
-
Lemma trivIsetS P Q :
P \subset Q → trivIset Q → trivIset P.
+
Lemma trivIsetS P Q :
P \subset Q → trivIset Q → trivIset P.
-
Lemma trivIsetI P D :
trivIset P → trivIset (
P ::&: D).
+
Lemma trivIsetI P D :
trivIset P → trivIset (
P ::&: D).
-
Lemma cover_setI P D :
cover (
P ::&: D)
\subset cover P :&: D.
+
Lemma cover_setI P D :
cover (
P ::&: D)
\subset cover P :&: D.
-
Lemma mem_pblock P x :
(x \in pblock P x) = (x \in cover P).
+
Lemma mem_pblock P x :
(x \in pblock P x) = (x \in cover P).
-
Lemma pblock_mem P x :
x \in cover P → pblock P x \in P.
+
Lemma pblock_mem P x :
x \in cover P → pblock P x \in P.
-
Lemma def_pblock P B x :
trivIset P → B \in P → x \in B → pblock P x = B.
+
Lemma def_pblock P B x :
trivIset P → B \in P → x \in B → pblock P x = B.
Lemma same_pblock P x y :
-
trivIset P → x \in pblock P y → pblock P x = pblock P y.
+
trivIset P → x \in pblock P y → pblock P x = pblock P y.
Lemma eq_pblock P x y :
-
trivIset P → x \in cover P →
-
(pblock P x == pblock P y) = (y \in pblock P x).
+
trivIset P → x \in cover P →
+
(pblock P x == pblock P y) = (y \in pblock P x).
Lemma trivIsetU1 A P :
-
{in P, ∀ B,
[disjoint A & B]} → trivIset P → set0 \notin P →
-
trivIset (
A |: P)
∧ A \notin P.
+
{in P, ∀ B,
[disjoint A & B]} → trivIset P → set0 \notin P →
+
trivIset (
A |: P)
∧ A \notin P.
-
Lemma cover_imset J F :
cover (
F @: J)
= \bigcup_(i in J) F i.
+
Lemma cover_imset J F :
cover (
F @: J)
= \bigcup_(i in J) F i.
-
Lemma trivIimset J F (
P :=
F @: J) :
-
{in J &, ∀ i j,
j != i → [disjoint F i & F j]} → set0 \notin P →
-
trivIset P ∧ {in J &, injective F}.
+
Lemma trivIimset J F (
P :=
F @: J) :
+
{in J &, ∀ i j,
j != i → [disjoint F i & F j]} → set0 \notin P →
+
trivIset P ∧ {in J &, injective F}.
-
Lemma cover_partition P D :
partition P D → cover P = D.
+
Lemma cover_partition P D :
partition P D → cover P = D.
-
Lemma card_partition P D :
partition P D → #|D| = \sum_(A in P) #|A|.
+
Lemma card_partition P D :
partition P D → #|D| = \sum_(A in P) #|A|.
Lemma card_uniform_partition n P D :
-
{in P, ∀ A,
#|A| = n} → partition P D → #|D| = #|P| × n.
+
{in P, ∀ A,
#|A| = n} → partition P D → #|D| = #|P| × n.
Section BigOps.
Variables (
R :
Type) (
idx :
R) (
op :
Monoid.com_law idx).
-
Let rhs_cond P K E :=
\big[op/idx]_(A in P) \big[op/idx]_(x in A | K x) E x.
-
Let rhs P E :=
\big[op/idx]_(A in P) \big[op/idx]_(x in A) E x.
+
Let rhs_cond P K E :=
\big[op/idx]_(A in P) \big[op/idx]_(x in A | K x) E x.
+
Let rhs P E :=
\big[op/idx]_(A in P) \big[op/idx]_(x in A) E x.
-
Lemma big_trivIset_cond P (
K :
pred T) (
E :
T → R) :
-
trivIset P → \big[op/idx]_(x in cover P | K x) E x = rhs_cond P K E.
+
Lemma big_trivIset_cond P (
K :
pred T) (
E :
T → R) :
+
trivIset P → \big[op/idx]_(x in cover P | K x) E x = rhs_cond P K E.
-
Lemma big_trivIset P (
E :
T → R) :
-
trivIset P → \big[op/idx]_(x in cover P) E x = rhs P E.
+
Lemma big_trivIset P (
E :
T → R) :
+
trivIset P → \big[op/idx]_(x in cover P) E x = rhs P E.
-
Lemma set_partition_big_cond P D (
K :
pred T) (
E :
T → R) :
-
partition P D → \big[op/idx]_(x in D | K x) E x = rhs_cond P K E.
+
Lemma set_partition_big_cond P D (
K :
pred T) (
E :
T → R) :
+
partition P D → \big[op/idx]_(x in D | K x) E x = rhs_cond P K E.
-
Lemma set_partition_big P D (
E :
T → R) :
-
partition P D → \big[op/idx]_(x in D) E x = rhs P E.
+
Lemma set_partition_big P D (
E :
T → R) :
+
partition P D → \big[op/idx]_(x in D) E x = rhs P E.
-
Lemma partition_disjoint_bigcup (
F :
I → {set T})
E :
-
(∀ i j,
i != j → [disjoint F i & F j]) →
-
\big[op/idx]_(x in \bigcup_i F i) E x =
-
\big[op/idx]_i \big[op/idx]_(x in F i) E x.
+
Lemma partition_disjoint_bigcup (
F :
I → {set T})
E :
+
(∀ i j,
i != j → [disjoint F i & F j]) →
+
\big[op/idx]_(x in \bigcup_i F i) E x =
+
\big[op/idx]_i \big[op/idx]_(x in F i) E x.
End BigOps.
@@ -1830,43 +1835,43 @@
Section Equivalence.
-
Variables (
R :
rel T) (
D :
{set T}).
+
Variables (
R :
rel T) (
D :
{set T}).
-
Let Px x :=
[set y in D | R x y].
-
Definition equivalence_partition :=
[set Px x | x in D].
-
Hypothesis eqiR :
{in D & &, equivalence_rel R}.
+
Let Px x :=
[set y in D | R x y].
+
Definition equivalence_partition :=
[set Px x | x in D].
+
Hypothesis eqiR :
{in D & &, equivalence_rel R}.
-
Let Pxx x :
x \in D → x \in Px x.
-
Let PPx x :
x \in D → Px x \in P :=
fun Dx ⇒
mem_imset _ Dx.
+
Let Pxx x :
x \in D → x \in Px x.
+
Let PPx x :
x \in D → Px x \in P :=
fun Dx ⇒
mem_imset _ Dx.
Lemma equivalence_partitionP :
partition P D.
Lemma pblock_equivalence_partition :
-
{in D &, ∀ x y,
(y \in pblock P x) = R x y}.
+
{in D &, ∀ x y,
(y \in pblock P x) = R x y}.
End Equivalence.
Lemma pblock_equivalence P D :
-
partition P D → {in D & &, equivalence_rel (
fun x y ⇒
y \in pblock P x)
}.
+
partition P D → {in D & &, equivalence_rel (
fun x y ⇒
y \in pblock P x)
}.
Lemma equivalence_partition_pblock P D :
-
partition P D → equivalence_partition (
fun x y ⇒
y \in pblock P x)
D = P.
+
partition P D → equivalence_partition (
fun x y ⇒
y \in pblock P x)
D = P.
Section Preim.
-
Variables (
rT :
eqType) (
f :
T → rT).
+
Variables (
rT :
eqType) (
f :
T → rT).
-
Definition preim_partition :=
equivalence_partition (
fun x y ⇒
f x == f y).
+
Definition preim_partition :=
equivalence_partition (
fun x y ⇒
f x == f y).
Lemma preim_partitionP D :
partition (
preim_partition D)
D.
@@ -1876,57 +1881,57 @@
Lemma preim_partition_pblock P D :
-
partition P D → preim_partition (
pblock P)
D = P.
+
partition P D → preim_partition (
pblock P)
D = P.
-
Lemma transversalP P D :
partition P D → is_transversal (
transversal P D)
P D.
+
Lemma transversalP P D :
partition P D → is_transversal (
transversal P D)
P D.
Section Transversals.
-
Variables (
X :
{set T}) (
P :
{set {set T}}) (
D :
{set T}).
+
Variables (
X :
{set T}) (
P :
{set {set T}}) (
D :
{set T}).
Hypothesis trPX :
is_transversal X P D.
-
Lemma transversal_sub :
X \subset D.
+
Lemma transversal_sub :
X \subset D.
Let tiP :
trivIset P.
-
Let sXP :
{subset X ≤ cover P}.
+
Let sXP :
{subset X ≤ cover P}.
-
Let trX :
{in P, ∀ B,
#|X :&: B| == 1
}.
+
Let trX :
{in P, ∀ B,
#|X :&: B| == 1
}.
Lemma setI_transversal_pblock x0 B :
-
B \in P → X :&: B = [set transversal_repr x0 X B].
+
B \in P → X :&: B = [set transversal_repr x0 X B].
-
Lemma repr_mem_pblock x0 B :
B \in P → transversal_repr x0 X B \in B.
+
Lemma repr_mem_pblock x0 B :
B \in P → transversal_repr x0 X B \in B.
-
Lemma repr_mem_transversal x0 B :
B \in P → transversal_repr x0 X B \in X.
+
Lemma repr_mem_transversal x0 B :
B \in P → transversal_repr x0 X B \in X.
-
Lemma transversal_reprK x0 :
{in P, cancel (
transversal_repr x0 X) (
pblock P)
}.
+
Lemma transversal_reprK x0 :
{in P, cancel (
transversal_repr x0 X) (
pblock P)
}.
-
Lemma pblockK x0 :
{in X, cancel (
pblock P) (
transversal_repr x0 X)
}.
+
Lemma pblockK x0 :
{in X, cancel (
pblock P) (
transversal_repr x0 X)
}.
-
Lemma pblock_inj :
{in X &, injective (
pblock P)
}.
+
Lemma pblock_inj :
{in X &, injective (
pblock P)
}.
-
Lemma pblock_transversal :
pblock P @: X = P.
+
Lemma pblock_transversal :
pblock P @: X = P.
-
Lemma card_transversal :
#|X| = #|P|.
+
Lemma card_transversal :
#|X| = #|P|.
-
Lemma im_transversal_repr x0 :
transversal_repr x0 X @: P = X.
+
Lemma im_transversal_repr x0 :
transversal_repr x0 X @: P = X.
End Transversals.
@@ -1939,9 +1944,9 @@
-
Lemma partition_partition (
T :
finType) (
D :
{set T})
P Q :
-
partition P D → partition Q P →
-
partition (
cover @: Q)
D ∧ {in Q &, injective cover}.
+
Lemma partition_partition (
T :
finType) (
D :
{set T})
P Q :
+
partition P D → partition Q P →
+
partition (
cover @: Q)
D ∧ {in Q &, injective cover}.
Variable T : finType.
-Notation sT := {set T}.
+Notation sT := {set T}.
Implicit Types A B C : sT.
-Implicit Type P : pred sT.
+Implicit Type P : pred sT.
-Definition minset P A := [∀ (B : sT | B \subset A), (B == A) == P B].
+Definition minset P A := [∀ (B : sT | B \subset A), (B == A) == P B].
-Lemma minset_eq P1 P2 A : P1 =1 P2 → minset P1 A = minset P2 A.
+Lemma minset_eq P1 P2 A : P1 =1 P2 → minset P1 A = minset P2 A.
Lemma minsetP P A :
- reflect ((P A) ∧ (∀ B, P B → B \subset A → B = A)) (minset P A).
+ reflect ((P A) ∧ (∀ B, P B → B \subset A → B = A)) (minset P A).
-Lemma minsetp P A : minset P A → P A.
+Lemma minsetp P A : minset P A → P A.
-Lemma minsetinf P A B : minset P A → P B → B \subset A → B = A.
+Lemma minsetinf P A B : minset P A → P B → B \subset A → B = A.
-Lemma ex_minset P : (∃ A, P A) → {A | minset P A}.
+Lemma ex_minset P : (∃ A, P A) → {A | minset P A}.
-Lemma minset_exists P C : P C → {A | minset P A & A \subset C}.
+Lemma minset_exists P C : P C → {A | minset P A & A \subset C}.
@@ -1993,40 +1998,38 @@
The 'locked_with' allows Coq to find the value of P by unification.
--
cgit v1.2.3