Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-26 19:37 587b312e

View on Github →

refactor(order/filter/basic): redefine filter.pure (#1889)

  • refactor(order/filter/basic): redefine filter.pure New definition has s ∈ pure a definitionally equal to a ∈ s.
  • Update src/order/filter/basic.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
  • Minor fixes suggested by @gebner
  • Fix compile
  • Update src/order/filter/basic.lean

Estimated changes

added theorem filter.join_pure
added theorem filter.le_pure_iff
deleted theorem filter.mem_pure
deleted theorem filter.mem_pure_iff
modified theorem filter.mem_pure_sets
added theorem filter.pure_bind
deleted theorem filter.pure_def
added theorem filter.pure_inj
added theorem filter.pure_sets
modified theorem filter.tendsto_const_pure
added theorem filter.tendsto_pure