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