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 →