Library Requisite.stdlib
Library Requisite.stdlib_wR
Library Requisite.ssr
Library Requisite.ssr_wMC
Library Logic.logic_compl
Library Logic.logic_tricks
Library Numbers.nat_compl
Library Numbers.countable_sets
Library Numbers.R_compl
Library Numbers.Numbers_wDep
Library Subsets.FinBij
Library Subsets.Subset
Library Subsets.Subset_dec
Library Subsets.Subset_charac
Library Subsets.Subset_finite
Library Subsets.Subset_any
Library Subsets.Subset_seq
Library Subsets.Function
- Brief description
- Description
- Additional support for functional extensionality
- Support for functions from/to types that are inhabited or not
- Additional support for image/preimage
- Additional support for the composition of functions
- Additional support for injective/surjective/bijective functions
- Support for the inverse of bijective functions
- Used logic axioms
- Usage
Library Subsets.Function_sub
Library Subsets.Sub_type
Library Subsets.Binary_relation
Library Subsets.ord_compl
Library Subsets.Finite_family
Library Subsets.Finite_table
Library Subsets.Subsets
Library Subsets.Subsets_wDep
Library Algebra.Hierarchy_compl
Library Algebra.Sub_struct
Library Algebra.Monoid.Monoid_compl
Library Algebra.Monoid.Monoid_FF
Library Algebra.Monoid.Monoid_FT
Library Algebra.Monoid.Monoid_sum
Library Algebra.Monoid.Monoid_morphism
Library Algebra.Monoid.Monoid_sub
Library Algebra.Monoid.MonoidMult
Library Algebra.Monoid.MonoidComp
Library Algebra.Monoid.ConcatnF
Library Algebra.Monoid.Monomial_order
Library Algebra.Monoid.Monoid
Library Algebra.Group.Group_compl
Library Algebra.Group.Group_morphism
Library Algebra.Group.Group_sub
Library Algebra.Group.GroupMult
Library Algebra.Group.Group
Library Algebra.Ring.Ring_compl
Library Algebra.Ring.Ring_FF_FT
Library Algebra.Ring.Ring_charac
Library Algebra.Ring.Ring_kron
Library Algebra.Ring.Ring_morphism
Library Algebra.Ring.Ring_sub
Library Algebra.Ring.Ring
Library Algebra.ModuleSpace.ModuleSpace_compl
Library Algebra.ModuleSpace.ModuleSpace_FF_FT
Library Algebra.ModuleSpace.ModuleSpace_lin_comb
Library Algebra.ModuleSpace.ModuleSpace_lin_map
Library Algebra.ModuleSpace.ModuleSpace_sub
Library Algebra.ModuleSpace.ModuleSpace_R_compl
Library Algebra.ModuleSpace.ModuleSpace
Library Algebra.AffineSpace.AffineSpace_def
Library Algebra.AffineSpace.AffineSpace_FF
Library Algebra.AffineSpace.AffineSpace_baryc
Library Algebra.AffineSpace.AffineSpace_aff_map
Library Algebra.AffineSpace.AffineSpace_sub
Library Algebra.AffineSpace.AffineSpace
Library Algebra.Finite_dim.matrix
Library Algebra.Finite_dim.Finite_dim_MS_def
Library Algebra.Finite_dim.Finite_dim_MS_lin_span
Library Algebra.Finite_dim.Finite_dim_MS_lin_gen
Library Algebra.Finite_dim.Finite_dim_MS_lin_indep
Library Algebra.Finite_dim.Finite_dim_MS_basis
Library Algebra.Finite_dim.Finite_dim_MS_lin_map
Library Algebra.Finite_dim.Finite_dim_MS_lin_indep_R
Library Algebra.Finite_dim.Finite_dim_MS_basis_R
Library Algebra.Finite_dim.Finite_dim_MS_lin_map_R
Library Algebra.Finite_dim.Finite_dim_MS_duality_R
Library Algebra.Finite_dim.Finite_dim_MS
Library Algebra.Finite_dim.Finite_dim_AS_def
Library Algebra.Finite_dim.Finite_dim_AS_aff_span
Library Algebra.Finite_dim.Finite_dim_AS_aff_gen
Library Algebra.Finite_dim.Finite_dim_AS_aff_indep
Library Algebra.Finite_dim.Finite_dim_AS_basis
Library Algebra.Finite_dim.Finite_dim_AS
Library Algebra.Finite_dim.Finite_dim
Library Algebra.binomial_compl
Library Algebra.Algebra
Library Algebra.Algebra_wDep
Library Lebesgue.subset_compl
Library Lebesgue.list_compl
Library Lebesgue.sort_compl
Library Lebesgue.R_compl
Library Lebesgue.LF_subcover
Library Lebesgue.Rbar_compl
Library Lebesgue.UniformSpace_compl
Library Lebesgue.topo_bases_R
Library Lebesgue.sum_Rbar_nonneg
Library Lebesgue.sigma_algebra
Library Lebesgue.sigma_algebra_R_Rbar
Library Lebesgue.Subset_system_def
Library Lebesgue.Subset_system_base
Library Lebesgue.Subset_system_gen
Library Lebesgue.Subset_system
Library Lebesgue.measurable_fun
Library Lebesgue.measure
Library Lebesgue.measure_uniq
Library Lebesgue.measure_R
Library Lebesgue.simple_fun
Library Lebesgue.Mp
Library Lebesgue.LInt_p
Library Lebesgue.Tonelli
Library Lebesgue.Lebesgue_p
Library Lebesgue.Lebesgue_p_wDep
Library Lebesgue.Bochner.square_bij
Library Lebesgue.Bochner.series
Library Lebesgue.Bochner.complete_normed_module_series
Library Lebesgue.Bochner.hierarchy_notations
Library Lebesgue.Bochner.Rmax_n
Library Lebesgue.Bochner.topology_compl
Library Lebesgue.Bochner.simpl_fun
Library Lebesgue.Bochner.CUS_Lim_seq
Library Lebesgue.Bochner.BInt_sf
Library Lebesgue.Bochner.Bsf_Lsf
Library Lebesgue.Bochner.Bi_fun
Library Lebesgue.Bochner.BInt_Bif
Library Lebesgue.Bochner.BInt_LInt_p
Library Lebesgue.Bochner.BInt_R
Library Lebesgue.Bochner.B_spaces
Library Lebesgue.Bochner.Bochner
Library Lebesgue.Bochner.Bochner_wDep
Library LM.fixed_point
Library LM.direct_sum
Library LM.hilbert
Library LM.continuous_linear_map
Library LM.hierarchyD
Library LM.lax_milgram
Library LM.lax_milgram_cea
Library LM.finitedim
- Finite dimensional subspaces : predicate approach
- Finite dimensional subspace closed
- Finite spaces : canonical structure approach
Library FEM.geometry
Library FEM.monomial
Library FEM.multi_index
Library FEM.poly_Pdk
Library FEM.geom_simplex
Library FEM.poly_LagPd1_ref
Library FEM.geom_transf_affine
Library FEM.poly_LagPd1_cur
Library FEM.poly_LagP1k
Library FEM.FE
Library FEM.FE_transf
Library FEM.FE_LagP
This page has been generated by coqdoc