Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.tendsto_lift

Modification history

2021-01-09 10:41

src/order/filter/lift.lean

feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)

Added filter.tendsto_lift View on Github →