lean_problem_sheets / 2019.questions.sheet3

source

theorem question_one_a_true (X Y Z : Type) (f : X → Y) (g : Y → Z) :

function.injective (g ∘ f) → function.injective f

Note: this declaration is incomplete and uses sorry.

source

theorem question_one_b_true (X Y Z : Type) (f : X → Y) (g : Y → Z) :

function.injective (g ∘ f) → function.injective g

Note: this declaration is incomplete and uses sorry.

source

theorem question_one_c_true (X Y Z : Type) (f : X → Y) (g : Y → Z) :

function.surjective (g ∘ f) → function.surjective f

Note: this declaration is incomplete and uses sorry.

source

theorem question_one_d_true (X Y Z : Type) (f : X → Y) (g : Y → Z) :

function.surjective (g ∘ f) → function.surjective g

Note: this declaration is incomplete and uses sorry.

source

noncomputable def fa :

ℝ → ℝ

Equations

fa = λ (x : ℝ), 1 / x

source

def fb :

ℝ → ℝ

Equations

fb = λ (x : ℝ), 2 * x + 1

source

def fc :

ℤ → ℤ

Equations

fc = λ (x : ℤ), 2 * x + 1

source

constant Riemann_Hypothesis :

Prop

source

noncomputable def fd :

ℝ → ℝ

Equations

fd = λ (x : ℝ), ite Riemann_Hypothesis (3 - x) (2 + x)

source

def fe :

ℤ → ℤ

Equations

fe = λ (n : ℤ), n ^ 3 - 2 * n ^ 2 + 2 * n - 1

source

theorem Q2a1 :

function.injective fa

Note: this declaration is incomplete and uses sorry.

source

theorem Q2a2 :

¬function.surjective fa

Note: this declaration is incomplete and uses sorry.

source

theorem Q2c3 :

function.bijective fc

Note: this declaration is incomplete and uses sorry.

source

theorem Q4a (X Y : Type) (f : X → Y) (g : Y → X) (h2sided : (∀ (x : X), g (f x) = x) ∧ ∀ (y : Y), f (g y) = y) :

(∀ (y : Y), f (g y) = y) ∧ ∀ (x : X), g (f x) = x

Note: this declaration is incomplete and uses sorry.

source

theorem exists_bijection_iff_has_two_sided_inverse (X Y : Type) :

(∃ (f : X → Y), function.bijective f) ↔ ∃ (f : X → Y) (g : Y → X), (∀ (x : X), g (f x) = x) ∧ ∀ (y : Y), f (g y) = y

source

theorem Q4b (X Y : Type) :

(∃ (f : X → Y), function.bijective f) ↔ ∃ (g : Y → X), function.bijective g

Note: this declaration is incomplete and uses sorry.

source

def friends {X Y Z : Type} (f : X → Z) (g : Y → Z) (hf : function.injective f) (hg : function.injective g) :

Prop

Equations

friends f g hf hg = ∃ (h : X → Y), function.bijective h ∧ f = g ∘ h

source

theorem Q5 (X Y Z : Type) (f : X → Z) (g : Y → Z) (hf : function.injective f) (hg : function.injective g) :

friends f g hf hg ↔ set.range f = set.range g

Note: this declaration is incomplete and uses sorry.