diff options
Diffstat (limited to 'mathcomp/ssreflect/fintype.v')
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 93810ca..c06238c 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -92,9 +92,9 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* enum_rank x == the i : 'I_(#|T|) such that enum_val i = x. *) (* enum_rank_in Ax0 x == some i : 'I_(#|A|) such that enum_val i = x if *) (* x \in A, given Ax0 : x0 \in A. *) -(* A \subset B == all x \in A satisfy x \in B. *) -(* A \proper B == all x \in A satisfy x \in B but not the converse. *) -(* [disjoint A & B] == no x \in A satisfies x \in B. *) +(* A \subset B <=> all x \in A satisfy x \in B. *) +(* A \proper B <=> all x \in A satisfy x \in B but not the converse. *) +(* [disjoint A & B] <=> no x \in A satisfies x \in B. *) (* image f A == the sequence of f x for all x : T such that x \in A *) (* (where a is an applicative predicate), of length #|P|. *) (* The codomain of F can be any type, but image f A can *) @@ -108,13 +108,13 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* im_y : y \in image f P. *) (* invF inj_f y == the x such that f x = y, for inj_j : injective f with *) (* f : T -> T. *) -(* dinjectiveb A f == the restriction of f : T -> R to A is injective *) +(* dinjectiveb A f <=> the restriction of f : T -> R to A is injective *) (* (this is a bolean predicate, R must be an eqType). *) -(* injectiveb f == f : T -> R is injective (boolean predicate). *) -(* pred0b A == no x : T satisfies x \in A. *) -(* [forall x, P] == P (in which x can appear) is true for all values of x; *) +(* injectiveb f <=> f : T -> R is injective (boolean predicate). *) +(* pred0b A <=> no x : T satisfies x \in A. *) +(* [forall x, P] <=> P (in which x can appear) is true for all values of x *) (* x must range over a finType. *) -(* [exists x, P] == P is true for some value of x. *) +(* [exists x, P] <=> P is true for some value of x. *) (* [forall (x | C), P] := [forall x, C ==> P]. *) (* [forall x in A, P] := [forall (x | x \in A), P]. *) (* [exists (x | C), P] := [exists x, C && P]. *) @@ -123,13 +123,15 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path. (* [exists x : T, P], [exists x : T in A, P], etc. *) (* -> The outer brackets can be omitted when nesting finitary quantifiers, *) (* e.g., [forall i in I, forall j in J, exists a, f i j == a]. *) -(* 'forall_pP == view for [forall x, p _], for pP : reflect .. (p _). *) -(* 'exists_pP == view for [exists x, p _], for pP : reflect .. (p _). *) +(* 'forall_pP <-> view for [forall x, p _], for pP : reflect .. (p _). *) +(* 'exists_pP <-> view for [exists x, p _], for pP : reflect .. (p _). *) +(* 'forall_in_pP <-> view for [forall x in .., p _], for pP as above. *) +(* 'exists_in_pP <-> view for [exists x in .., p _], for pP as above. *) (* [pick x | P] == Some x, for an x such that P holds, or None if there *) (* is no such x. *) (* [pick x : T] == Some x with x : T, provided T is nonempty, else None. *) (* [pick x in A] == Some x, with x \in A, or None if A is empty. *) -(* [pick x in A | P] == Some x, with x \in A s.t. P holds, else None. *) +(* [pick x in A | P] == Some x, with x \in A such that P holds, else None. *) (* [pick x | P & Q] := [pick x | P & Q]. *) (* [pick x in A | P & Q] := [pick x | P & Q]. *) (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *) |