![hbhb bbk](/uploads/mathdown/20201125233739.jpg)



&&&def ref
$$
ref\ U\ R:=\forall x:U,R \ x\ x
$$
&&&




&&&def total
$$
total\ U\ R:=\forall x\ y,R\ x\ y\lor R\ y \ x\
$$
&&&



&&&exc
$$
\forall U(R:U\rightarrow U\rightarrow Prop),total\ R\rightarrow ref \ R
$$

&&&
```
Require Import Utf8.

Set Implicit Arguments.

Definition imp(a b:Prop):=a → b.

Definition ref U R:=∀x:U,R x x.

Definition total U R:=∀x y:U,R x y∨R y x.

Goal ∀U(R:U → U → Prop),total R → ref R.
Abort.
```




全順序における反射条件の冗長性

この記事を高評価した人

この記事に送られたバッジ

投稿者

コメント

他の人のコメント