Module mathcomp.classical.mathcomp_extra
From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
# MathComp extra
This files contains lemmas and definitions recently added in mathcomp,
in order to be able to compile analysis with older versions of mathcomp.
```
proj i f == f i, where f : forall i, T i
dfwith f x == fun j => x if j = i, and f j otherwise
given x : T i
```
Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
MathComp 2.3 additions
Module
Order
Source code
.Source code
Import Order.
Definition
default_display
Source code
: disp_t.sigT_fun : forall {I : Type} {X : I -> Type} {T : Type}, (forall i : I, X i -> T) -> {i : I & X i} -> T sigT_fun is not universe polymorphic Arguments sigT_fun {I}%type_scope {X}%function_scope {T}%type_scope f%function_scope x sigT_fun is transparent Expands to: Constant mathcomp.classical.unstable.sigT_fun Declared in library mathcomp.classical.unstable, line 464, characters 11-19
Source code
End Order.
Definition
proj
Source code
{} { : I -> Type} ( : forall , T i) := f i.Source code
Section DFunWith.
Variables ( : eqType) ( : I -> Type) ( : forall , T i).
Definition
dfwith
Source code
( : T i) ( : I) : T j :=Source code
if (i =P j) is ReflectT ij then ecast (T j) ij x else f j.
Lemma
dfwithin
Source code
: dfwith x i = x.Source code
Lemma
dfwithout
Source code
( : T i) : i != j -> dfwith x j = f j.Source code
Variant
dfwith_spec
Source code
( : T i) : forall , T j -> Type :=Source code
|
DFunWithin
Source code
: dfwith_spec x xSource code
|
DFunWithout
Source code
: i != j -> dfwith_spec x (f j).Source code
Lemma
dfwithP
Source code
( : T i) ( : I) : dfwith_spec x (dfwith x j).Source code
Lemma
projK
Source code
( : T i) : cancel (@dfwith i) (proj i).Source code
End DFunWith.
Arguments dfwith {I T} f i x.
MathComp 2.4 additions
MathComp 2.5 additions
Section ssralg.
Lemma
subrKC
Source code
{ : zmodType} ( : V) : x + (y - x) = y.Source code
End ssralg.
Lemma
sumr_le0
Source code
( : numDomainType) ( : seq I) ( : pred I) ( : I -> R) :Source code
(forall , P i -> F i <= 0)%R -> (\sum_( <- r | P i) F i <= 0)%R.
Lemma
card_fset_sum1
Source code
( : choiceType) ( : {fset T}) :Source code
#|` A| = (\sum_( <- A) 1)%N.
Proof.
Lemma
lteifS
Source code
{Source code
disp
Source code
: Order.disp_t} { : porderType disp}Source code
[ : T] ( : bool) : (x < y)%O -> (x < y ?<= if C)%O.
Proof.
MathComp 2.6 additions
Lemma
intrD1
Source code
{ : pzRingType} ( : int) : (i + 1)%:~R = i%:~R + 1 :> R.Source code
Proof.
Lemma
intr1D
Source code
{ : pzRingType} ( : int) : (1 + i)%:~R = 1 + i%:~R :> R.Source code