# ITP Blatt 05

Besprechung: am 11.06.2026

```
{-# OPTIONS --allow-unsolved-metas #-}
open import Level as L using (Level)
open import Data.Product
open import Data.Sum
open import Data.Nat
open import Data.Nat.Properties using (m≤m⊔n; m≤n⊔m; ≤-trans)
open import Data.List
open import Data.List as List using (List; _++_; cartesianProduct)
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
  using (∈-++⁺ˡ; ∈-++⁺ʳ; ∈-map⁺; ∈-cartesianProduct⁺)
open import Relation.Nullary using (¬_; Dec; yes; no; map′)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions hiding (Decidable)
open import Relation.Unary using (_⊆_; Decidable)


module _ where
private 
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'
    C : Set ℓ''

open import Finite
```

## Finiteness of sums
Zeigen Sie, dass endliche Mengen unter Disjunktion Vereinigungen abgeschlossen sind.
Nutzen Sie die oben importierten Hilfsfunktionen.
```
⊎-finite : FiniteL A → FiniteL B → FiniteL (A ⊎ B)
⊎-finite A-fin B-fin = {! !}
```
## Finiteness of products
Zeigen Sie, dass endliche Mengen unter Produkten abgeschlossen sind.
Nutzen Sie die oben importierten Hilfsfunktionen.
```
×-finite : FiniteL A → FiniteL B → FiniteL (A × B)
×-finite A-fin B-fin = {! !}
```

## Finiteness and quantifiers
Vervollständigen Sie folgenden Beweis aus der Vorlesung:
```
module Finite-Quantifiers-Blatt {X : Set ℓ} (P : X → Set ℓ) (P? : Decidable P) where
  Finite⇒Dec∀∈ : ∀ (l : List X) → Dec ((_∈ l) ⊆ P)
  Finite⇒Dec∀∈ = {! !}
  -- Finite⇒Dec∀∈ [] = yes (λ ())
  -- Finite⇒Dec∀∈ (x ∷ l) with (P? x)
  -- ... | no ¬Px = no (λ x∷l⊆P → ¬Px (x∷l⊆P (here refl)))
  -- ... | yes Px = map′ {!!} {!!} (Finite⇒Dec∀∈ l)
  -- Hinweis: beim verwenden von map′ müssen Sie die beiden Richtungen
  -- extra in 'where' definieren, damit Agda's Typinferenz richtig funktioniert.

  Finite⇒decidable : FiniteL X → Dec (∀ x → P x)
  Finite⇒decidable = {! !}
```

## ℕ not finite
Zeigen Sie, dass ℕ nicht endlich ist:
Tipp: Nutzen Sie oben importierte funktionen zu `⊔`.
```
ℕ-not-finite : ¬ FiniteL ℕ
ℕ-not-finite = {! !}
```