Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 09:56 efe794c3

View on Github →

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

Estimated changes

Modified src/dynamics/omega_limit.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

Modified src/order/filter/basic.lean

modified theorem filter.tendsto_id'

modified theorem filter.tendsto_id

Modified src/topology/instances/ennreal.lean

Modified src/topology/order.lean

added theorem continuous_id_iff_le

Modified src/topology/separation.lean