mathlib3
efe794c3 - chore(order/filter): turn `tendsto_id'` into an `iff` lemma (#14791)

Commit

3 years ago

chore(order/filter): turn `tendsto_id'` into an `iff` lemma (#14791)

Author

urkud

urkud

Parents

Loading