mathlib3
feat(topology/continuous_on): add `tendsto_nhds_within_iff_seq_tendsto`
#17261
Open
Open
feat(topology/continuous_on): add `tendsto_nhds_within_iff_seq_tendsto` #17261
RemyDegenne
wants to merge
7 commits into
master
from
RD_tendsto_seq
add tendsto_nhds_within_iff
65cdafc8
Merge remote-tracking branch 'origin/RD_tendsto_within' into RD_tends…
e970f07b
add tendsto_nhds_within_iff_seq_tendsto
34d38919
RemyDegenne
commented
on 2022-10-30
Update src/topology/continuous_on.lean
7ceb5fe1
Merge remote-tracking branch 'origin/master' into RD_tendsto_seq
0fc4843e
urkud
commented
on 2022-11-05
add tendsto_inf_principal_iff_seq_tendsto
d2320f2f
fix, golf
a3678b5a
urkud
commented
on 2022-11-05
Reviewers
Assignees
No one assigned
Labels
awaiting-author
t-topology
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub