namespace http://mathhub.info/MitM/core/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
theory Functions : base:?Logic =
include ?Relations ❙
function_composition: {A : type,B : type, C : type} (A ⟶ B) ⟶ (B ⟶ C) ⟶ (A ⟶ C) ❘ = [A,B,C][f,g] [x] g (f x) ❘ # 5 ° 4 ❙
image: {A,B} (A ⟶ B) ⟶ set A ⟶ set B ❘ # im 3 4 ❙
function_restriction: {A : type,B : type, C : type}{prf : (C <* A)} (A ⟶ B) ⟶ (C ⟶ B) ❘ # function_restriction 5 3 ❙
preimage : {A,B} (A ⟶ B) ⟶ set B ⟶ set A ❘ # preim 3 4 ❙
identityFunction : {A : type} (A ⟶ A) ❘ = [A,x] x ❘ # Id 1 ❙
constantFunction : {A : type,B : type} B ⟶ A ⟶ B ❘ = [A,B,c,x] c ❙
❚
theory Injective : base:?Logic =
injective : {A : type,B : type, f: A ⟶ B} prop ❘
= [A,B,f] ∀[x:A] ∀[y : A] f x ≐ f y ⇒ x ≐ y ❘
# is_injective 3 ❙
❚
theory Surjective : base:?Logic =
surjective : {A : type, B : type, f: A ⟶ B} prop ❘
= [A,B,f] ∀[y : B] ∃[x: A] f x ≐ y ❘
# is_surjective 3 ❙
❚
theory Bijective : base:?Logic =
include ?Surjective❙
include ?Injective❙
bijective : {A: type, B: type, f : A ⟶ B} prop ❘
= [A, B, f] is_injective f ∧ is_surjective f❘
# is_bijective 3❙
bijections : {A : type, B : type} type ❘ = [A, B] (A ⟶ B) ❘ # bijections 1 2❙
inverseBijections : {A : type, B : type} bijections A B ⟶ bijections B A ❘ # bijinv 3❙
❚
theory InverseFunction : base:?Logic =
include ☞base:?DescriptionOperator ❙
inverse : {A : type,B: type, f: A ⟶ B} B ⟶ A ❘
= [A,B,f,y] ι [x] f x ≐ y ❘
# 1^-1 ❙
❚
theory Permutation : base:?Logic =
include ?Bijective ❙
permutation : {A: type, f: A ⟶ A} prop ❘
= [A,f] is_bijective f ❘
# is_permutation 2 ❙
❚