math-comp/analysis

Issues

• useless instantiation?

  #1253 opened a day ago by affeldt-aist
  0

• Missing subspace lemma on balls

  #1231 opened 3 days ago by CohenCyril
  1

• `to_set` -> `xsection`

  #1248 opened 4 days ago by affeldt-aist
  0

• better advertise the `coq-mathcomp-classical`

  #1126 opened 6 months ago by affeldt-aist
  4

• update using MathComp 1.17.0 naming convention

  #1241 opened 8 days ago by affeldt-aist
  0

• update `uniform_bigO.v`

  #1141 opened 11 days ago by affeldt-aist
  2

• `setD_closed` and `setDI_closed`

  #1225 opened a month ago by affeldt-aist
  0

• generalization of `lime_sup` lemmas to `limf_sup`

  #1135 opened 6 months ago by affeldt-aist
  0

• put together statements about `]x-r,x+r[`

  #1084 opened 8 months ago by affeldt-aist
  0

• `inf_lower_bound` and `inf_lb`

  #1226 opened 23 days ago by affeldt-aist
  0

• typo in `functions.v`'s doc

  #1236 opened 23 days ago by affeldt-aist
  0

• dead code in `realfun.v`

  #1237 opened 23 days ago by affeldt-aist
  0

• use `patch` here?

  #1100 opened 7 months ago by affeldt-aist
  0

• naming and definition of `monotonous`

  #1133 opened 6 months ago by affeldt-aist
  1

• Splitting `topology.v`

  #1167 opened 5 months ago by zstone1
  1

• improve the documentation of `contra.v`

  #1197 opened 3 months ago by affeldt-aist
  0

• rename the `misc` subdir to `showcase`

  #1233 opened 25 days ago by affeldt-aist
  1

• small generalization of Markov's lemma

  #1232 opened 25 days ago by affeldt-aist
  1

• shorten proof about monotonic functions

  #1156 opened 5 months ago by affeldt-aist
  0

• naming

  #1229 opened 25 days ago by affeldt-aist
  1

• finitely-supported probability measure

  #1227 opened a month ago by affeldt-aist
  0

• move `mulr_rev` ?

  #1092 opened 2 months ago by affeldt-aist
  1

• location of the definition of `expR`

  #1219 opened 2 months ago by affeldt-aist
  0

• `notin_set` vs. `in_setE`

  #1190 opened 2 months ago by affeldt-aist
  0

• `distribution` in probability.v is inconsistent with its documentation

  #1185 opened 2 months ago by t6s
  1

• typo

  #1208 opened 2 months ago by affeldt-aist
  0

• Countable product of measurable spaces

  #1214 opened 2 months ago by t6s
  0

• spurious integrability condition

  #1212 opened 2 months ago by affeldt-aist
  0

• Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

  #1187 opened 3 months ago by rtetley
  5

• `gee_pmull`: hypo `0 < x` can be slightly generalized

  #1203 opened 3 months ago by affeldt-aist
  0

• what means the `m` suffix

  #1094 opened 3 months ago by affeldt-aist
  3

• moving contents from `cantor.v` to `topology.v`

  #1105 opened 3 months ago by affeldt-aist
  0

• Notation of cvg can be broken

  #1195 opened 3 months ago by IshiguroYoshihiro
  0

• renaming of `Measure_isSFinite_subdef`?

  #1182 opened 3 months ago by affeldt-aist
  0

• HB failing when installing of 0.7.0 with opam

  #1169 opened 5 months ago by affeldt-aist
  1

• `ge0_integralZr` is lacking

  #1178 opened 4 months ago by affeldt-aist
  0

• typo, duplicate

  #1176 opened 4 months ago by affeldt-aist
  0

• Experiment with Export and categories in contra.v

  #1157 opened 5 months ago by proux01
  0

• Release with support with more recent Coq and mathcomp

  #1120 opened 5 months ago by SnarkBoojum
  5

• `nbhsx_ballx` : `{posnum R}` or `R`?

  #1131 opened 5 months ago by affeldt-aist
  1

• Lacking a Proof command

  #1114 opened 6 months ago by affeldt-aist
  0

• the proof of `cvg_at_rightP` should be shorter

  #1134 opened 6 months ago by affeldt-aist
  0

• unsusable lemma

  #1123 opened 6 months ago by affeldt-aist
  0

• move `ae_eq`?

  #1096 opened 6 months ago by IshiguroYoshihiro
  0

• lnX -> lnXn

  #1093 opened 7 months ago by hoheinzollern
  0

• Add `cantor.v` to `theories/Make`

  #1098 opened 7 months ago by affeldt-aist
  0

• lacks a `Proof` command

  #1103 opened 7 months ago by affeldt-aist
  0

• non-informative comment

  #1104 opened 7 months ago by affeldt-aist
  0

• Is `cantor_pseudoMetric` necessary?

  #1099 opened 7 months ago by affeldt-aist
  0

• lacks a `Proof` keyword

  #1086 opened 8 months ago by affeldt-aist
  0