mathlib3
feat(analysis/locally_convex/with_seminorms): equicontinuity criterions
#17275
Open
Overview
Commits
257
Changes
View On GitHub
Commits
  • Swap uniform inducing !
    ADedecker committed 3 years ago
  • Pi swap part2
    ADedecker committed 3 years ago
  • Remove exit
    ADedecker committed 3 years ago
  • Small fix
    ADedecker committed 3 years ago
  • Use notation
    ADedecker committed 3 years ago
  • First part done for 𝔖-convergence
    ADedecker committed 3 years ago
  • Setup for precomp
    ADedecker committed 3 years ago
  • Precomp uniform continuous
    ADedecker committed 3 years ago
  • Finished ?
    ADedecker committed 3 years ago
  • Move things
    ADedecker committed 3 years ago
  • Docs
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Begin
    ADedecker committed 3 years ago
  • Content
    ADedecker committed 3 years ago
  • Fix doc
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Small fix
    ADedecker committed 3 years ago
  • Fix
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Tmp (this won't compile)
    ADedecker committed 3 years ago
  • Add Pi version of `arrow_prod_equiv_prod_arrow`
    ADedecker committed 3 years ago
  • Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Change approach
    ADedecker committed 3 years ago
  • Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Use uniform_equiv
    ADedecker committed 3 years ago
  • Setup
    ADedecker committed 3 years ago
  • Make phi explicit, suggestions from review
    ADedecker committed 3 years ago
  • Remove useless restriction
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Fix; add congr and prod
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Fix
    ADedecker committed 3 years ago
  • Def doc
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Finished
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Useless import
    ADedecker committed 3 years ago
  • Begin
    ADedecker committed 3 years ago
  • Basis of directed [b]infi
    ADedecker committed 3 years ago
  • Merge branch 'basis_infi_directed' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Bases for topology/uniform structure of 𝔖-convergence
    ADedecker committed 3 years ago
  • Dedup
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Better parameters, lint failures
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_comp2
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Minor tweaks
    PatrickMassot committed 3 years ago
  • Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Fix
    ADedecker committed 3 years ago
  • Start writing more docs
    ADedecker committed 3 years ago
  • Use notations
    ADedecker committed 3 years ago
  • More docs
    ADedecker committed 3 years ago
  • Lots of comments
    ADedecker committed 3 years ago
  • Finish doc, add missing lemmas!
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Fix and comments
    ADedecker committed 3 years ago
  • Better docstring and comments
    ADedecker committed 3 years ago
  • initial commit
    YaelDillies committed 3 years ago
  • kill nonneg'
    YaelDillies committed 3 years ago
  • typos
    YaelDillies committed 3 years ago
  • fix analysis.seminorm
    YaelDillies committed 3 years ago
  • seminorm classes
    YaelDillies committed 3 years ago
  • group norms
    YaelDillies committed 3 years ago
  • nolint
    YaelDillies committed 3 years ago
  • Merge branch 'seminorm_class' into group_norm
    YaelDillies committed 3 years ago
  • kill cores
    YaelDillies committed 3 years ago
  • fix analysis.normed_space.operator_norm
    YaelDillies committed 3 years ago
  • fix analysis.normed_space.continuous_affine_map
    YaelDillies committed 3 years ago
  • fix analysis.inner_product_space.basic
    YaelDillies committed 3 years ago
  • fix analysis.normed_space.lp_space
    YaelDillies committed 3 years ago
  • fix measure_theory.function.lp_space
    YaelDillies committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_group
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_bases
    ADedecker committed 3 years ago
  • Begin
    ADedecker committed 3 years ago
  • Criterions
    ADedecker committed 3 years ago
  • Merge branch 'AD_uniform_convergence_bases' into AD_equicontinuous
    ADedecker committed 3 years ago
  • Bump, bases
    ADedecker committed 3 years ago
  • Test
    ADedecker committed 3 years ago
  • Go back
    ADedecker committed 3 years ago
  • Go back again
    ADedecker committed 3 years ago
  • Let's do that later
    ADedecker committed 3 years ago
  • Progress
    ADedecker committed 3 years ago
  • Closure, finish fixing everything
    ADedecker committed 3 years ago
  • Uniform equicontinuity on compact spaces
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_equicontinuous
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_equicontinuous
    ADedecker committed 3 years ago
  • Docs
    ADedecker committed 3 years ago
  • backport map_nonneg
    YaelDillies committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into kill_normed_group_core
    YaelDillies committed 3 years ago
  • bump
    YaelDillies committed 3 years ago
  • ++
    ADedecker committed 3 years ago
  • + more commits ...
FAQ Terms Privacy Refunds Impressum
Loading