Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-08 10:42 0b81b249

View on Github →

feat(analysis/topological_structures): add tendsto_of_tendsto_of_tendsto_of_le_of_le

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/topology/topological_structures.lean

added theorem tendsto_of_tendsto_of_tendsto_of_le_of_le

modified theorem tendsto_orderable