mathlib3
feat(topology/continuous_on): add `tendsto_nhds_within_iff_seq_tendsto`
#17261
Open
Overview
Commits
7
Changes
View On GitHub
Commits
  • add tendsto_nhds_within_iff
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/RD_tendsto_within' into RD_tendsto_seq
    RemyDegenne committed 3 years ago
  • add tendsto_nhds_within_iff_seq_tendsto
    RemyDegenne committed 3 years ago
  • Update src/topology/continuous_on.lean
    RemyDegenne committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into RD_tendsto_seq
    RemyDegenne committed 3 years ago
  • add tendsto_inf_principal_iff_seq_tendsto
    RemyDegenne committed 3 years ago
  • fix, golf
    RemyDegenne committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading