Lean Lab 🧪

	/-
	Sina Hazratpour
	Introduction to Proof
	MATH 301, Johns Hopkins University, Spring 2022
	-/

	import tactic

	/- We want to show that in order to establish a bijection between two sets (that is a function which is both an injection and a surjection ), it is enough to establish an isomorphism (i.e. a function which has a two-sided inverse.)
	-/
	variables {A B : Type}
	lemma inverse_of_left_inverse_and_right_inverse (f : A → B) (g : B → A) (h : B → A) :
	(f ∘ g = id) → (h ∘ f = id) → h = g :=
	begin
	intros hp hq,
	funext,
	calc
	h x = (h ∘ id) x : rfl
	... = (h ∘ (f ∘ g)) x : by rw hp
	... = (h ∘ f) (g x) : rfl -- this rfl is used to prove associativity of composition
	... = id (g x) : by rw hq
	... = g x : rfl,
	end

	@[simp] def isIso (f : A → B) := ∃ g: B → A, (g ∘ f = id) ∧ (f ∘ g = id )

	-- by using lemma `left_and_right_inverses_are_equal`
	lemma iso_of_left_and_right_inverse (f : A → B) (g : B → A) (h : B → A) :
	(f ∘ g = id) → (h ∘ f = id) → isIso f:=
	begin
	intros hp hq,
	have he : h = g, from inverse_of_left_inverse_and_right_inverse f g h hp hq,
	use g,
	split,
	{rw ← he, exact hq},
	{exact hp},
	end

	-- Recall
	@[simp] def isInjective {X Y : Type} (f : X → Y) : Prop :=
	∀ ⦃x₁ x₂⦄, f x₁ = f x₂ → x₁ = x₂

	@[simp] def isSurjective {X Y : Type} (f : X → Y) : Prop :=
	∀ y : Y, ∃ x : X, f x = y

	def isBijection (f: A → B) := isInjective f ∧ isSurjective f

	theorem isos_are_bijections (f : A → B) : isIso f → isBijection f :=
	begin
	intro hp,
	simp at hp,
	cases hp with g hpg,
	split,
	{ simp,
	intros a b hq,
	calc
	a = id a : by refl
	... = (g ∘ f) (a) : by rw ←hpg.1
	... = g ( f (a)) : by refl
	... = g (f b ) : by rw hq
	... = (g ∘ f) b : by refl
	... = id b : by rw hpg.1
	... = b : by refl,
	},
	{simp,
	intro y,
	have u : (f ∘ g) y = id y, by rw hpg.2,
	simp at u,
	exact ⟨g y, u ⟩,
	},
	end


	/-
	CHALLENGE: Can you prove the converse, that is every bijection is an isomorphism?
	-/

view raw MATH301_iso_bijection.lean hosted with ❤ by GitHub

	/-
	Sina Hazratpour, Johns Hopkins University
	MATH301 Lecture for the section on Friday, Apr 1, 2022.
	Key words: Retracts, Sections, Injections, Surjections
	-/

	import tactic
	import init.data.set
	open nat

	variables X Y Z U V W: Type

	/-
	A retract (aka left inverse) of a function f: A → B is a function r: B → A such that r ∘ f = id_A. In this situation we also say A is a retract of B.
	-/
	def isRetract {X Y : Type} (r : X → Y) : Prop := ∃ s : Y → X, r ∘ s = id

	-- pred : ℕ → ℕ is a retract of succ: ℕ → ℕ
	lemma pred_of_succ : pred ∘ succ = id
	:=
	begin
	funext,
	refl,
	end

	-- challenge
	example : succ ∘ pred ≠ id
	:=
	begin
	intro h,
	have e : (succ ∘ pred) 0 = id 0, by rw h,
	simp at e,
	exact e,
	end

	/-
	A section (aka right inverse) of function f : A → B is a function s: B → A such that f ∘ s = id_B.
	-/

	def isSection {X Y : Type} (s : X → Y) : Prop := ∃ r : Y → X, r ∘ s = id

	/- From the example above we know that `succ` is a section of `pred`; we use `use` tactic, which is similar to `existsi`, to prove this.
	-/
	theorem succ_is_section : isSection succ :=
	begin
	use [pred, pred_of_succ],
	end

	/-
	A function f: A → B is injective (also called one-to-one) whenever the following sentence holds.
	∀ a, b :A, f(a) = f(b) → a = b
	An injective function is said to be an injection.
	-/
	def isInjective {X Y : Type} (f : X → Y) : Prop :=
	∀ ⦃x₁ x₂⦄, f x₁ = f x₂ → x₁ = x₂


	-- Let's prove the identity function is injective:
	lemma injective_id : isInjective (id : X → X) :=
	begin
	intros x₁ x₂,
	intro hp,
	dsimp at hp,
	exact hp,
	end


	/-
	Let's prove the following theorem from the lecture:
	Every section is injective.

	PROOF:
	Suppose f: A → B is a section with a retract r: B → A. Therefore, r ∘ f = id_A.
	For arbitrary elements a and a' of A, suppose f(a) = f(a'). It follows that
	a = id (a) = r ∘ f (a) = r ( f(a) ) = r(f(a')) = r ∘ f (a') = id_A (a') = a'.
	Hence, f is injective.
	-/

	-- challenge: translate the proof above to Lean.
	theorem injective_section (s : Y → X ): isSection s → isInjective s :=
	begin
	sorry,
	end


	/-
	There is an empty type in Lean: `empty`. This type has no element, but, for any type `A` it comes with a recursor function `empty.elim : empty → A`.
	-/
	#check empty
	#check empty.elim

	/-
	First we show that for any type A there is a unique function from the empty type `empty` to A. Then we show this unique function is injective.
	-/

	theorem fun_from_empty_unique {A : Type} (f g : empty → A) : f = g :=
	begin
	funext,
	exact empty.elim x,
	end

	-- Therefore, any function `empty → A` is necessarily equal to `empty.elim`.
	theorem only_empty_elim {A : Type} (f : empty → A) : f = empty.elim :=
	begin
	apply fun_from_empty_unique f empty.elim,
	end

	theorem injective_empty (A : Type) : isInjective (empty.elim : empty → A) :=
	begin
	intros x x' h,
	exact empty.elim x',
	end


	-- Injections are closed under composition.
	lemma injective_comp (f : X → Y) (g : Y → Z) (inj_f : isInjective f) (inj_g : isInjective g): isInjective (g ∘ f) :=
	begin
	intros x x' h,
	simp at h,
	have h₂ : f x = f x', from inj_g h,
	exact inj_f h₂,
	end


	def isSurjective {X Y : Type} (f : X → Y) : Prop :=
	∀ y : Y, ∃ x : X, f x = y


	/-
	challenge: Prove the following theorem in Lean:
	Theorem: Every retract is surjective.
	-/


	-- Surjections are closed under composition.
	lemma surj_comp (f : X → Y) (g : Y → Z) (surj_f : isSurjective f) (surj_g : isSurjective g): isSurjective (g ∘ f) :=
	begin
	intro z,
	have h₁, from surj_g z,
	cases h₁ with y h₂,
	have h₃, from surj_f y,
	cases h₃ with x h₄,
	have h₅: g y = g (f (x)), by rw h₄,
	have h₆ : z = g (f (x)), by rw [←h₂, h₅],
	existsi x,
	rw h₆,
	end

view raw MATH301_InjSurj.lean hosted with ❤ by GitHub

	/-
	Sina Hazratpour
	Introduction to Proof
	MATH 301, Johns Hopkins University, Spring 2022
	-/

	import init.classical
	import init.data.set
	import data.set
	import data.set.basic
	import data.real.basic
	import tactic.ring
	import analysis.special_functions.exp
	import analysis.special_functions.trigonometric.basic
	import data.set.intervals.infinite


	/- ## Images -/


	open complex


	noncomputable theory
	#check real.sin

	/-
	The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
	which one can derive all its properties. For explicit bounds on π, see `data.real.pi.bounds`.
	protected noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero
	-/

	#check real.sin real.pi



	variables X Y Z U V W: Type

	-- We must `open set` in order to use `image` and `preimage`; otherwise we have to use a more cumbersome notation like set.image which is less than ideal.
	open set
	open function



	section image
	variables A B S : set U
	variable f : A → B
	variables g h : U → V
	#check A
	#check B
	#check f
	/-
	Coercion of sets into types:
	A : U → Prop
	ι : Prop → Type
	↥A is ι ∘ A : U → Type gotten by the code of the comprhension type { x : U // A x }
	Claim: { x : U \| A x} is the same set as the truncation of ι ∘ A.
	-/
	#check ↥A
	#check g
	#check image
	#check image g
	#check image g S
	#check image h S
	#check g '' S
	-- if g is π_1 : ℝ × ℝ to ℝ and S is a subset of ℝ × ℝ then images g S is a subset of ℝ.
	-- recall that `image g S` is defined to be the set `{ y : V \| ∃ x : U, x ∈ S ∧ g x = y }`
	-- A hypothesis ``y ∈ g '' S`` decomposes to a triple ``⟨x, hxS, e⟩`` with ``x : U`` satisfying the hypotheses ``hxS : x ∈ S`` and ``e : g x = y``.
	-- The information `y ∈ g ''S` is the same as a triple for some `x:U` where `hxS: x ∈ S` and `e : gx = y`.
	--another notation of `image g S` is `g'' S`.
	end image



	namespace example_from_analysis

	#check real.sin
	def f (x : ℝ) : ℝ := real.sin x
	#check f
	#check f real.pi

	/- The sine of `π` is `0`. -/
	/- idea: how do we prove that sin π is zero?
	Well, π is define as 2 * π/2 where π/2 is the root of cos : ℝ → ℝ
	between 1 and 2.
	sin π = sin (2 * π/2 )= sin (π + π /2) = sin(π/2 + π/2) = sin (π/2) cos(π/2) + cos(π_2) sin(π_2) = sin (π/2) * 0 + 0 * sin (π/2) = 0 + 0 = 0.
	-/
	@[simp] lemma sin_pi_is_zero : real.sin (real.pi) = 0 :=
	begin
	rw [← mul_div_cancel_left real.pi (@two_ne_zero ℝ _ _), two_mul, add_div, real.sin_add, real.cos_pi_div_two],
	simp,
	end

	/-- The sine of `π / 6` is `1 / 2`. -/
	@[simp] lemma sin_pi_div_six_is_half : real.sin (real.pi / 6) = 1 / 2 :=
	begin
	rw [← real.cos_pi_div_two_sub, ← real.cos_pi_div_three],
	congr,
	ring,
	end

	-- Find f({0, π/6}), f([0, π/6]), f([π/6, π/2]), f([0, π/2]).
	lemma image_i : real.sin '' ( {real.pi/6, real.pi} ) = {0, 1/2} :=
	begin
	sorry,
	end

	#check Icc
	-- `Icc 0 (real.pi/6)` is the closed interval [0, π/6]
	lemma image_ii : f '' Icc 0 (real.pi/6) = Icc 0 (1/2) := sorry
	lemma image_iii : f '' Icc (real.pi/6) (real.pi/2) = Icc (1/2) 1 := sorry
	lemma image_iv : f '' Icc 0 (real.pi/2) = Icc 0 1 := sorry
	end example_from_analysis




	/-! ## Preimages -/

	section preimage
	variables A B : Type
	variable f : A → B
	#check B
	variable T : set V
	variable g : U → V
	#check g
	#check preimage g
	variable y : V
	#check preimage g T
	#reduce preimage g T
	-- Another notation for `preimage g T` is `g ⁻¹' T`. You can get by typing "g", "\", "^", "-1", and "'".
	-- `preimage g T` is defined by the set `{ x : U \| g x ∈ T } : set U`
	#check preimage g {y}
	end preimage



	/-! ### Images and Preimages: Some Theorems -/

	/-
	The subset relationship is respected by the image operation.
	-/
	theorem image_increasing {U V : Type*} {f : U → V} {S T : set U} {h : S ⊆ T}: image f S ⊆ image f T
	:=
	begin
	rw subset_def,
	intros y hy,
	-- what was the definition of `f '' S` b/c we have to use hy.
	-- { y : V \| ∃ x : U, x ∈ S ∧ f x = y }
	cases hy with x hxS,
	have hxT : x ∈ T, from h hxS.1,
	-- what is `f '' T`? acoording to its defn, it is { y : V \| ∃ x : U, x ∈ T ∧ f x = y }
	existsi x,
	constructor,
	exact hxT,
	exact hxS.2,
	end


	theorem image_increasing_alt {U V : Type*} {f : U → V} {S T : set U} {h : S ⊆ T}: image f S ⊆ image f T
	:=
	begin
	rw subset_def,
	intros y hy,
	-- what was the definition of `f '' S` b/c we have to use hy.
	-- { y : V \| ∃ x : U, x ∈ S ∧ f x = y }
	cases hy with x hxS,
	have hxT : x ∈ T, from h hxS.1,
	-- what is `f '' T`? acoording to its defn, it is { y : V \| ∃ x : U, x ∈ T ∧ f x = y }
	existsi x,
	exact ⟨ hxT, hxS.2⟩,
	end


	-- The subset relationship is also respected by the preimage operation.
	lemma preimage_increasing {U V : Type*} {f : U → V} {S T : set V} {h : S ⊆ T}: preimage f S ⊆ preimage f T
	:=
	begin
	intro x,
	simp,
	apply h,
	end

	-- Preimage operation preserve the intersection of sets.
	-- "meet" is another name for intersection.

	lemma preimage_preserves_meets {U V : Type*} {f : U → V} {S T : set V}: f ⁻¹' (S ∩ T) = f ⁻¹' S ∩ f ⁻¹' T :=
	by { ext, refl }


	lemma image_of_meet {U V : Type*} {f : U → V} {S T : set U}: f '' (S ∩ T) ⊆ f '' S ∩ f '' T :=
	-- by {ext, refl } fails
	begin
	sorry,
	end

	/- However the reverse subset inclusion is not true: Consider the constant function
	λ n, 1 : ℕ → ℕ -/

	@[simp] def cons_at_zero : ℕ → ℕ := λ n, 0
	#check cons_at_zero


	/-
	We write @[simp] at the beginning of a definition/lemma/theorem X to tell Lean that it can use `simp` tactic in other definition/lemma/theorem which use X.
	-/
	@[simp] def Even : set ℕ := { n : ℕ \| even n}
	@[simp] def Odd : set ℕ := { n : ℕ \| odd n}


	lemma even_meet_odd : Even ∩ Odd = ∅ :=
	begin
	ext n,
	simp,
	end

	lemma zero_is_even : 0 ∈ Even :=
	by {simp}

	lemma image_counterexample₁ : cons_at_zero '' Even = { 0 }
	:=
	begin
	ext n,
	split,
	-- as we learned before `rintro` is for recursive introduction of conjunction and existential qunatifiers.
	{
	rintro ⟨ m, hm, e ⟩ ,
	dsimp at e,
	simp at hm,
	simp,
	rw ←e,
	},
	{
	intro h,
	simp at h,
	rw h,
	exact ⟨ 0, zero_is_even, rfl ⟩,
	},

	end

	lemma one_is_odd : 1 ∈ Odd :=
	by {simp}

	lemma image_counterexample₂ : cons_at_zero '' Odd = { 0 }
	:=
	begin
	ext n,
	split,
	-- as we learned before `rintro` is for recursive introduction of conjunction and existential qunatifiers.
	{
	rintro ⟨ m, hm, e ⟩ ,
	dsimp at e,
	simp at hm,
	simp,
	rw ←e,
	},
	{
	intro h,
	simp at h,
	rw h,
	exact ⟨ 1, one_is_odd, rfl ⟩,
	},
	end

	-- meet of images is not the image of meet.
	example :
	¬ (cons_at_zero '' Even) ∩ (cons_at_zero '' Odd) ⊆ cons_at_zero '' (Even ∩ Odd)
	:=
	begin
	rw even_meet_odd,
	rw image_counterexample₁,
	rw image_counterexample₂,
	simp,
	end


	-- Image respects singletons
	lemma image_preserves_singelton {U V : Type*} {f : U → V} {u : U} : f '' { u } = { f u } :=
	begin
	ext y,
	split,
	{
	rintros ⟨x, hx, e⟩,
	simp,
	simp at hx,
	rw [←e, hx]
	},
	intro h,
	simp,
	simp at h,
	exact h,
	end

	-- "join" is another name for union
	lemma image_preserves_joins₁ {U V : Type*} {f : U → V} {S T : set U}: f '' (S ∪ T) = f '' S ∪ f '' T :=
	begin
	ext y,
	simp,
	split,
	intros h,
	cases h with x hx,
	cases hx.1 with hx₁ hx₂,
	{
	apply or.inl,
	existsi x,
	sorry,
	},
	{sorry},
	sorry,
	end

	/-
	Here is a shorter proof relying on the fact that a hypothesis `y ∈ g '' S` decomposes to a triple `⟨x, hxS, e⟩` with `x : U` satisfying the hypotheses `hxS : x ∈ S` and `e : g x = y`.
	-/

	lemma image_preserves_joins₂ {U V : Type*} {f : U → V} {S T : set U}: f '' (S ∪ T) = f '' S ∪ f '' T := begin
	ext y,
	split,
	rintros ⟨x, hxS \| hxT, rfl⟩,
	left, use [x, hxS],
	right, use [x, hxT],
	rintros ( ⟨x, hxS, rfl⟩ \| ⟨x, hxT, rfl⟩ ),
	use [x, or.inl hxS],
	use [x, or.inr hxT],
	end



	-- A family (A_i \| i ∈ I) of sets (in the universe M) is formalized as a function A : I → set U of types.

	example {M N: Type} {I : Type*} (A : I → set M) (B : I → set N) (f : M → N) : f '' (⋃ i, A i) = ⋃ i, f '' A i :=
	begin
	ext y,
	simp,
	split,
	{ rintros ⟨x, ⟨i, xAi⟩, fxeq⟩,
	use [i, x, xAi, fxeq] },
	rintros ⟨i, x, xAi, fxeq⟩,
	exact ⟨x, ⟨i, xAi⟩, fxeq⟩,
	end



	theorem Frobenius_reciprocity {U V : Type*} {f : U → V} {A : set U} {B : set V } :
	B ∩ f '' A = f '' (f ⁻¹' B ∩ A )
	:=
	begin
	sorry,
	end

view raw MATH301_image_preimage.lean hosted with ❤ by GitHub

	/-
	Sina Hazratpour
	Introduction to Proof
	MATH 301, Johns Hopkins University, Spring 2022
	-/


	import init.data.set
	import data.set
	import data.set.basic


	open set
	open function
	open nat

	variables X Y Z U V W : Type


	-- Recall
	def isInjective {X Y : Type} (f : X → Y) : Prop :=
	∀ ⦃x₁ x₂⦄, f x₁ = f x₂ → x₁ = x₂

	def isSurjective {X Y : Type} (f : X → Y) : Prop :=
	∀ y : Y, ∃ x : X, f x = y



	/- ## Example 1 : Functions on Natural Numbers -/

	/-
	- CHALLENGE 1: Define the subsets of even and odd numbers
	-/

	@[simp] def my_even (n : ℕ) := ∃ k : ℕ, n = k + k
	#check my_even
	@[simp] def Even := { n : ℕ \| my_even n}
	#check Even

	@[simp] def my_odd (n : ℕ) := ∃ k : ℕ, n = k + k + 1
	#check my_odd
	@[simp] def Odd := { n : ℕ \| my_odd n}
	#check Odd


	/-
	- CHALLENGE 2: Prove that 0 is even and 1 is odd.
	-/

	@[simp] lemma zero_is_even : 0 ∈ Even :=
	begin
	use 0,
	end


	@[simp] lemma one_is_odd : 1 ∈ Odd :=
	begin
	use 0,
	end


	/-
	CHALLENGE 3: Prove that the odd numbers and even numbers do not meet, i.e. their intersection is the empty set.
	-/

	#check add_left_cancel
	lemma eq_zero_of_add_right_eq_self {m n : ℕ } : (m + n = m) → (n = 0) :=
	begin
	intro h,
	rw ← add_zero m at h,
	rw add_assoc m 0 n at h,
	rw zero_add n at h,
	rw add_left_cancel h,
	end



	lemma odd_meet_even : Even ∩ Odd = ∅ :=
	begin
	ext,
	rw inter_def,
	simp,
	intros k hk l,
	intro h,
	rw hk at h,
	sorry,
	end


	/- CHALLENGE 4: Define the constant function at 0 from ℕ to ℕ. -/

	@[simp] def constant_at_zero : ℕ → ℕ := λ n, 0

	/- CHALLENGE 5: Show that the image of the constant function at zero of the even numbers is the singleton containing zero. -/

	#check constant_at_zero ''

	lemma image_of_constant_zero : constant_at_zero '' Even = { 0 } :=
	begin
	ext y,
	split,
	{ intro hy,
	cases hy with x hx,
	simp,
	simp at hx,
	have hxr, from hx.2,
	exact eq.symm hxr,
	},
	{
	intro h,
	simp,
	use [0, 0, rfl],
	simp at h,
	exact eq.symm h,
	},
	end



	/-
	CHALLENGE 6: Show that the image of the constant function at zero of the odd numbers is the singleton containing zero.
	-/

	/-
	In general we have:
	-/
	lemma imagee_of_meet {f : X → Y} (S T : set X) : f '' (S ∩ T) ⊆ f '' S ∩ f '' T :=
	begin
	rw subset_def,
	intros y hy,
	cases hy with x hx,
	simp,
	simp at hx,
	exact ⟨ exists.intro x ⟨ hx.1.1, hx.2⟩ , exists.intro x ⟨ hx.1.2, hx.2⟩ ⟩,
	end


	/-
	CHALLENGE 7 : Use 1-6 to prove that in general the meet of images is not the image of meet.
	-/



	/-
	CHALLENGE 8: Investigate under what conditions the the meet of images is the image of meet.
	-/

	lemma image_of_injections_preserves_meets {X Y : Type} {f : X → Y} {S T : set X}: isInjective f → f '' (S ∩ T) = f '' S ∩ f '' T :=
	begin
	sorry,
	end




	/- ## Examples 2: Image of finite sets -/

	/-
	- CHALLENGE 1: Prove that the image of a singleton set is singelton.
	-/

	lemma image_preserves_singelton {U V : Type*} {f : U → V} {u : U} : f '' { u } = { f u } :=
	begin
	sorry,
	end

	/-
	- CHALLENGE 2: Prove that the image operation respects unions of sets.
	-/

	lemma image_preserves_joins {U V : Type*} {f : U → V} {S T : set U}: f '' (S ∪ T) = f '' S ∪ f '' T :=
	begin
	sorry,
	end





	/-
	- CHALLENGE 3: Use the previous two results to prove that for any function g : bool → bool, we have g ''({tt,ff}) = {g tt, g ff}
	-/



	/-
	## Example 3: Subsingletons
	-/

	/-- A set `S` is a `subsingleton`, if it has at most one element. -/

	def subsingle {X : Type} (S : set X) : Prop :=
	∀ ⦃x y : X⦄ (hx : x ∈ S) (hy : y ∈ S), x = y

	#check subsingle


	/-
	- CHALLENGE 1: Prove that a subsingleton T of a subsingleton S of X is a subsingleton of X.
	-/

	lemma subsingle_of_subsingle {S T : set X} (hS : subsingle S) (hT : T ⊆ S) : subsingle T :=
	begin
	sorry,
	end


	/-
	- CHALLENGE 2: Prove that the image of a subsingleton S of X under any function f: X → Y is a subsingleton of Y.
	-/

	lemma image_of_subsingle {f : X → Y} {S : set X}(hS : subsingle S) : subsingle (f '' S) :=
	begin
	sorry,
	end


	/-
	- CHALLENGE 3: Any singelton is a subsingleton.
	-/


	/-
	- CHALLENGE 4: Any inhabited subsingleton is a singelton.
	-/

	lemma inhabited_subsingleton_is_singelton {S : set X} (hS : subsingle S) {x : X} (hx : x ∈ S) : S = {x} := sorry


	/--
	- CHALLENGE 5: A subset of a singleton set is a subsingleton.
	--/




	/-
	- CHALLENGE 6: The empty set is a subsingelton.
	-/

	lemma empty_is_a_subsingleton :
	subsingle (∅ : set X) := sorry

	/-
	- CHALLENGE 7: Prove that the law of excluded middle implies that the only subsingletons are the empty and singeltons. How unbecoming!
	-/



	/-
	## Example 4: Restrict of the functions
	-/


	/-
	Suppose f: A → B is a function and U ⊆ A. We can restrict the function f to U, that is we restrict the action of f to those elements of A which are already present in U.
	For instance if we restrict the absolute value function to the set of positive real numbers we obtain the identity function on the set of positive real numbers.
	In Lean we prefer types to sets for defining functions. So if f : X → Y and P : X → Prop then we can restrict f to the type { x : X // P x }:
	the restriction of f then takes a : { x : X // P x }to f a.
	-/

	def restrict (f : X → Y) (P : X → Prop) :
	{ x : X // P x } → Y := λ ⟨ x, p ⟩, f x

	/-
	- CHALLENGE 1: Restrict the function λ n : ℕ, n² to the odd numbers.

	- CHALLENGE 2: Show that the image of the restricted function is a subset of odd numbers.

	- CHALLENGE 3: Show that a restriction of a restriction is again a restriction.
	-/



	/-
	## Example 5 : The Galois Connection
	-/


	theorem Galois_connection {X Y : Type} (f: X → Y) (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f ⁻¹' T :=
	begin
	split,
	{ intros h x xS,
	have fxS : f x ∈ f '' S,
	from mem_image_of_mem _ xS,
	exact h fxS },
	{ intros h y yS,
	rcases yS with ⟨x, xS, fxey⟩,
	rw ← fxey,
	apply h xS },
	end


	#check subset_refl
	#check subset_rfl


	/-
	We use the Galois connection between the image and preimage operations to prove that every set is contained in the preimage of its image.
	-/

	example (f : X → Y) (S : set X) : S ⊆ f ⁻¹' (f '' S) :=
	begin
	have u, from Galois_connection f S (f '' S),
	exact iff.elim_left u subset_rfl,
	end

	/-
	Morover, if the function f is injective the subset inclusion above is in fact equality.
	-/
	example {f : X → Y} (inj_f : isInjective f) (S : set X) : S = f ⁻¹' (f '' S) :=
	begin
	sorry,
	end

	/-
	Does the condition S = f ⁻¹' (f '' S) for all subsets S : set X imply injectivity of f?
	-/

	example {f : X → Y} : ∀ (S : set X), S = f ⁻¹' (f '' S) → isInjective f :=
	begin
	sorry,
	end

view raw MATH301_inj_surj_examples.lean hosted with ❤ by GitHub