Cookies disclaimer

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

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

Download Files

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
Download Files

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
Download Files

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

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
Download Files

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
Download Files

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