Finite Field
30-sec diagnosis
Back to NPA

Module

Mathlib.Logic.Prop

npa-mathlib

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Theorems

6

Definitions

0

Inductive types

0

Axioms

0

Declarations

imp_chain4

forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (S : Prop), forall (pq : forall (p : P), Q), forall (qr : forall (q : Q), R), forall (rs : foral...

theorem

imp_permute3

forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (S : Prop), forall (h : forall (p : P), forall (q : Q), forall (r : R), S), forall (r : R), fora...

theorem

imp_apply_twice

forall (P : Prop), forall (h : forall (p : P), P), forall (p : P), P

theorem

imp_const3

forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (p : P), forall (q : Q), forall (r : R), P

theorem

imp_flip_chain

forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (qr : forall (q : Q), R), forall (pq : forall (p : P), Q), forall (p : P), R

theorem

imp_higher_apply

forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (h : forall (f : forall (p : P), Q), R), forall (f : forall (p : P), Q), R

theorem

Hashes

source
sha256:466c82f2aa00708bbf9d91d7e59a5f0a629f5f61af979711c325a0f4ce29dec6
certificateFile
sha256:890b8b619cf965a9cf530efbd7b05287c49867af9489357f87918d7ef53fbd14
export
sha256:2be3062e9adb565d319e67b416e96dd6c5f5ec6bb4fa9fd1902c256bf06c8613
axiomReport
sha256:70b2d0f35f9ebfff46bdf399b80487f0c76ffd6460ab930f733af1f889d2fc65
certificate
sha256:91e5f7856e09d29a80903fe50932f3a340bc446965b2ae3d414cdbbef5b39cf5

Source

theorem imp_chain4 :
  forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (S : Prop), forall (pq : forall (p : P), Q), forall (qr : forall (q : Q), R), forall (rs : forall (r : R), S), forall (p : P), S :=
  fun P => fun Q => fun R => fun S => fun pq => fun qr => fun rs => fun p => rs (qr (pq p))

theorem imp_permute3 :
  forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (S : Prop), forall (h : forall (p : P), forall (q : Q), forall (r : R), S), forall (r : R), forall (p : P), forall (q : Q), S :=
  fun P => fun Q => fun R => fun S => fun h => fun r => fun p => fun q => h p q r

theorem imp_apply_twice :
  forall (P : Prop), forall (h : forall (p : P), P), forall (p : P), P :=
  fun P => fun h => fun p => h (h p)

theorem imp_const3 :
  forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (p : P), forall (q : Q), forall (r : R), P :=
  fun P => fun Q => fun R => fun p => fun q => fun r => p

theorem imp_flip_chain :
  forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (qr : forall (q : Q), R), forall (pq : forall (p : P), Q), forall (p : P), R :=
  fun P => fun Q => fun R => fun qr => fun pq => fun p => qr (pq p)

theorem imp_higher_apply :
  forall (P : Prop), forall (Q : Prop), forall (R : Prop), forall (h : forall (f : forall (p : P), Q), R), forall (f : forall (p : P), Q), R :=
  fun P => fun Q => fun R => fun h => fun f => h f