Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Infinity Hotel

Infinity Hotel has an infinite number of rooms numbered 0, 1, … and serves an infinite number of guests with personal identifiers 0, 1, …. All guests want a room of their own.

A finite subset of the guests S are VIPs that always stay in a room that is specifically prepared for them. This assignment of VIPs to rooms is given by an injection f.

You are given the following tasks:

1. Show that the hotel can serve the VIPs and all other guests. That is, show that there is an injection g from all the guests to the room numbers that respects f on S.

2. Show that the hotel can serve the VIPs and all other guests and also fill all its rooms. That is, show that there is a bijection h between all the guests and the room numbers that respects f on S.

Thanks to Simon Wimmer for stating the problem. Thanks to Armaël Guéneau and Kevin Kappelmann for translating.

## Resources

### Definitions File

```theory Defs
imports "HOL-Library.Infinite_Set"
begin

end
```

### Template File

```theory Submission
imports Defs
begin

text ‹Task 1 - 1/5 points›
theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
sorry

text ‹Task 2 - 4/5 points›
theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
using assms by (rule Submission.injective_embedding)

theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
using assms by (rule Submission.bijective_embedding)

end
```

### Definitions File

```-- Lean version: 3.4.2
-- Mathlib version: 2019-09-11

import data.finset
open function

-- Coercion from finite sets to sets
@[simp] protected def finset.coe_set {α : Type*} : has_coe (finset α) (set α) := ⟨finset.to_set⟩

-- The goals used in submission
notation `GOAL_INJECTIVE` :=
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ ↪ ℕ), restrict h S = f
notation `GOAL_BIJECTIVE` :=
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ restrict h S = f```

### Template File

```import .defs

open function
local attribute [instance] finset.coe_set
local infixr `|` :100 := restrict -- write f|S for restrict f S

-- 1/5 points
lemma submission_injective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ ↪ ℕ), h|S = f := sorry

-- 4/5 points
theorem submission_bijective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ h|S = f := sorry```

### Check File

```import .defs
import .submission

open function
local attribute [instance] finset.coe_set

theorem goal_injective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ ↪ ℕ), restrict h S = f :=
@submission_injective

theorem goal_bijective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ restrict h S = f :=
@submission_bijective```

### Definitions File

```Require Export ConstructiveEpsilon.
Require Export List Lia.
Export ListNotations.

Definition inj {A B : Type} (f : A -> B) :=
forall a a', f a = f a' -> a = a'.

Definition inj_on {A B : Type} (P : A -> Prop) (f : A -> B) :=
forall a a', P a -> P a' -> f a = f a' -> a = a'.

Definition surjective {A B : Type} (f : A -> B) :=
forall b, exists a, f a = b.

Definition bij {A B : Type} (f : A -> B) :=
exists g, (forall a, g (f a) = a) /\ (forall b, f (g b) = b).

Coercion is_true (b : bool) := b = true.```

### Template File

```Require Import Defs.

Section InfinityHotel.

Variable VIP : nat -> bool.
Variable VIP_bound : nat.
Hypothesis VIP_bounded : forall x, VIP x -> x < VIP_bound.

Variable f : nat -> nat.
Variable f_inj : inj_on VIP f.

(* 1/5 points *)
Theorem task1 : exists g, inj g /\ forall x, VIP x -> g x = f x.

(* This will be useful *)
Check constructive_indefinite_ground_description_nat_Acc.

Lemma inj_surj_bij (g : nat -> nat) : inj g -> surjective g -> bij g.

(* 4/5 points *)
Theorem task2 : exists g, bij g /\ forall x, VIP x -> g x = f x.

End InfinityHotel.```

### Definitions File

```theory Defs
imports "HOL-Library.Infinite_Set"
begin

end
```

### Template File

```theory Submission
imports Defs
begin

text ‹Task 1 - 1/5 points›
theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
sorry

text ‹Task 2 - 4/5 points›
theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
using assms by (rule Submission.injective_embedding)

theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
using assms by (rule Submission.bijective_embedding)

end
```

### Definitions File

```-- Lean version: 3.16.2
-- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955

import tactic.basic data.finset
open function

-- Coercion from finite sets to sets
-- @[simp] protected def finset.coe_set {α : Type*} : has_coe (finset α) (set α) := ⟨λ S, ↑S⟩

-- The goals used in submission
notation `GOAL_INJECTIVE` :=
∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), set.restrict h ↑S = f
notation `GOAL_BIJECTIVE` :=
∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ set.restrict h ↑S = f```

### Template File

```import .defs

open function
local infixr `|` :100 := set.restrict -- write f|S for restrict f S

-- 1/5 points
lemma submission_injective :
∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), h|↑S = f := sorry

-- 4/5 points
theorem submission_bijective :
∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ h|↑S = f := sorry```

### Check File

```import .defs
import .submission

open function
local attribute [instance] finset.coe_set

theorem goal_injective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ ↪ ℕ), restrict h S = f :=
@submission_injective

theorem goal_bijective :
∀ {S : finset ℕ} (f : S ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ restrict h S = f :=
@submission_bijective```

### Definitions File

```theory Defs
imports "HOL-Library.Infinite_Set"
begin

end
```

### Template File

```theory Submission
imports Defs
begin

text ‹Task 1 - 1/5 points›
theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
sorry

text ‹Task 2 - 4/5 points›
theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

theorem injective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃g. inj_on g ℕ ∧ (∀x ∈ S. g x = f x)"
using assms by (rule Submission.injective_embedding)

theorem bijective_embedding:
fixes f :: "nat ⇒ nat"
and S :: "nat set"
assumes "inj_on f S" and "finite S"
shows "∃h. bij_betw h ℕ ℕ ∧ (∀x ∈ S. h x = f x)"
using assms by (rule Submission.bijective_embedding)

end
```

Terms and Conditions