Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[flicky frans]

Ah, I see, the question was about (¬ isFinite P) ⊎ (¬ isFinite Q).

2014-11-01 0:20 GMT+03:00, flicky frans <flickyfrans at gmail.com>:
>>modulo some de Morgan and contraposition obfuscation
>
> But isn't it possible to reduce the amount of this obfuscation in the
> statement, having
>
> open import Relation.Nullary
> open import Data.Product
> open import Data.Sum
>
> lem : ∀ (P Q : Set) -> ¬ ¬ ((¬ P) ⊎ (¬ Q)) -> ¬ (P × Q)
> lem P Q f p = f (λ {(inj₁ g) -> g (proj₁ p) ; (inj₂ g) -> g (proj₂ p)})
>
> ? Or am I missing something trivial?
>
> 2014-10-31 23:45 GMT+03:00, Andreas Abel <abela at chalmers.se>:
>>
>>
>> On 31.10.14 8:05 PM, Nils Anders Danielsson wrote:
>>> On 2014-10-25 17:18, Sergei Meshveliani wrote:
>>>> I have been asked about a constructive proof of this theorem:
>>>>
>>>>    ℕ ⊆ P U Q -> (¬ isFinite P) ⊎ (¬ isFinite Q).
>>>
>>> Some respondents have noted things that are not provable. The following
>>> statement is provable:
>>>
>>>    ¬ isFinite (P ∪ Q) → ¬ ¬ ((¬ isFinite P) ⊎ (¬ isFinite Q))
>>>
>>> See Data.Nat.InfinitelyOften in the standard library.
>>
>> Which is a direct consequence of the positive statement
>>
>>    _∪-Finite_ : ∀ {P Q} → Finite P → Finite Q → Finite (P ∪ Q)
>>
>> modulo some de Morgan and contraposition obfuscation.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>