I agree 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 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:

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*.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.

Download Files
### Definitions File

### Template File

### Check File

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

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

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

Download Files
### Definitions File

### Template File

### Check 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

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

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

Download Files
### Definitions File

### Template 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.

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. Admitted. (* This will be useful *) Check constructive_indefinite_ground_description_nat_Acc. Lemma inj_surj_bij (g : nat -> nat) : inj g -> surjective g -> bij g. Admitted. (* 4/5 points *) Theorem task2 : exists g, bij g /\ forall x, VIP x -> g x = f x. Admitted. End InfinityHotel.

Download Files
### Definitions File

### Template File

### Check File

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

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

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

Download Files
### Definitions File

### Template File

### Check 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

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

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

Download Files
### Definitions File

### Template File

### Check File

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

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

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