# Theory Functions

```section ‹Functions›

theory Functions
imports "../Extensions/Set_Extensions"
begin

locale bounded_function =
fixes A :: "'a set"
fixes B :: "'b set"
fixes f :: "'a ⇒ 'b"
assumes wellformed[intro?, simp]: "x ∈ A ⟹ f x ∈ B"

locale bounded_function_pair =
f: bounded_function A B f +
g: bounded_function B A g
for A :: "'a set"
and B :: "'b set"
and f :: "'a ⇒ 'b"
and g :: "'b ⇒ 'a"

locale injection = bounded_function_pair +
assumes left_inverse[simp]: "x ∈ A ⟹ g (f x) = x"
begin

lemma inj_on[intro]: "inj_on f A" using inj_onI left_inverse by metis

lemma injective_on:
assumes "x ∈ A" "y ∈ A" "f x = f y"
shows "x = y"
using assms left_inverse by metis

end

locale injective = bounded_function +
assumes injection: "∃ g. injection A B f g"
begin

definition "g ≡ SOME g. injection A B f g"

sublocale injection A B f g unfolding g_def using someI_ex[OF injection] by this

end

locale surjection = bounded_function_pair +
assumes right_inverse[simp]: "y ∈ B ⟹ f (g y) = y"
begin

lemma image_superset[intro]: "f ` A ⊇ B"
using g.wellformed image_iff right_inverse subsetI by metis

lemma image_eq[simp]: "f ` A = B" using image_superset by auto

end

locale surjective = bounded_function +
assumes surjection: "∃ g. surjection A B f g"
begin

definition "g ≡ SOME g. surjection A B f g"

sublocale surjection A B f g unfolding g_def using someI_ex[OF surjection] by this

end

locale bijection = injection + surjection

lemma inj_on_bijection:
assumes "inj_on f A"
shows "bijection A (f ` A) f (inv_into A f)"
proof
show "⋀ x. x ∈ A ⟹ f x ∈ f ` A" using imageI by this
show "⋀ y. y ∈ f ` A ⟹ inv_into A f y ∈ A" using inv_into_into by this
show "⋀ x. x ∈ A ⟹ inv_into A f (f x) = x" using inv_into_f_f assms by this
show "⋀ y. y ∈ f ` A ⟹ f (inv_into A f y) = y" using f_inv_into_f by this
qed

end
```