Coq로 증명
반대칭 관계에 최대한 존재한다면
Example hantaisyo U R:=
forall a b:U,R a b->R b a->a=b:Prop.
Example saidaigen U(R:U->U->Prop)a:=
forall x,R x a.
Goal forall U(R:U->U->Prop)a b,
hantaisyo U R->
saidaigen U R a->
saidaigen U R b->
a=b.
Proof.
intros.
unfold hantaisyo in H.
specialize(H a b).
unfold saidaigen in H0.
unfold saidaigen in H1.
specialize(H0 b).
specialize(H1 a).
specialize(H H1 H0).
clear H0 H1 R.
case H.
clear b H.
reflexivity.
Qed.
Reference
이 문제에 관하여(Coq로 증명), 우리는 이곳에서 더 많은 자료를 발견하고 링크를 클릭하여 보았다 https://zenn.dev/sabataro/articles/e57f9261bcf622803f46텍스트를 자유롭게 공유하거나 복사할 수 있습니다.하지만 이 문서의 URL은 참조 URL로 남겨 두십시오.
우수한 개발자 콘텐츠 발견에 전념
(Collection and Share based on the CC Protocol.)
좋은 웹페이지 즐겨찾기
