Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-09 10:41 a161256c

View on Github →

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

Estimated changes

Modified src/order/filter/interval.lean

Modified src/order/filter/lift.lean

added theorem filter.lift'_infi_powerset

added theorem filter.tendsto_lift'

added theorem filter.tendsto_lift

Modified src/topology/algebra/ordered.lean