[Isarmathlib-devel] Function lemma

isarmathlib-devel

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Isarmathlib-devel] Function lemma

From:	Sanghyeon Seo
Subject:	[Isarmathlib-devel] Function lemma
Date:	Tue, 17 Jun 2008 12:10:13 +0900

I tried to prove the following statement, but I can't.

lemma X:
  assumes "f : A -> B" and "ALL x:A. f`(x):C"
  shows "f : A -> C"

-- 
Seo Sanghyeon

[Prev in Thread]

Current Thread

[Next in Thread]

[Isarmathlib-devel] Function lemma, Sanghyeon Seo <=
- Re: [Isarmathlib-devel] Function lemma, Slawomir Kolodynski, 2008/06/17

Prev by Date: Re: [Isarmathlib-devel] Re: Polynomial ring
Next by Date: Re: [Isarmathlib-devel] Function lemma
Previous by thread: [Isarmathlib-devel] Polynomial ring
Next by thread: Re: [Isarmathlib-devel] Function lemma
Index(es):
- Date
- Thread