Library Waterproof.Notations.Functions

Require Import Waterproof.Libs.Functions.
Require Import Waterproof.Notations.Sets.

Declare a scope for function-related notations

Declare Scope function_scope.

Notations for function images and preimages

The notation gU for the image of set U under function g

Notation "g [ U ]" := (image g U) (at level 10) : function_scope.

The notation f⁻¹V for the preimage of set V under function f

Notation "f ⁻¹ [ V ]" := (preimage f V) (at level 10) : function_scope.

Function Composition

The notation g ∘ f for the composition of functions g and f This matches the mathematical convention where (g ∘ f)(x) = g(f(x))

Notation "g ∘ f" := (composition f g) (at level 40, left associativity) : function_scope.

Notation "f 'is' 'injective'" := (injective f) (at level 68) : function_scope.

Notation "f 'is' 'surjective'" := (surjective f) (at level 68) : function_scope.

Notation "f 'is' 'bijective'" := (bijective f) (at level 68) : function_scope.

Notation "f 'has' 'a' 'left' 'inverse'" := (has_left_inverse f) (at level 68) : function_scope.

Notation "f 'is' 'a' 'left' 'inverse' 'of' g" := (left_inverse g f) (at level 68) : function_scope.

Notation "f 'has' 'a' 'right' 'inverse'" := (has_right_inverse f) (at level 68) : function_scope.

Notation "f 'is' 'a' 'right' 'inverse' 'of' g" := (right_inverse g f) (at level 68) : function_scope.

Notation "f 'has' 'an' 'inverse'" := (has_inverse f) (at level 68) : function_scope.

Notation "f 'is' 'an' 'inverse' 'of' g" := (inverse g f) (at level 68) : function_scope.