Finite Field
30秒診断
NPAへ戻る

Declaration

not_intro

Mathlib.Logic.Iff

Packages

2

Module

63

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Statement

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

Proof term

fun P => fun h => h

Constants

Mathlib.Logic.Iff.False

Interface hash: sha256:d9ca31ab11c822de78350f077307aa8ad9671d60cfb6d77584b33bdc4286c11b

Mathlib.Logic.Iff.Not

Interface hash: sha256:e2a4a4c5eb00336cb3f1318ac11972d6d1feaae5e9b54865be4ce0115e989c6c