Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-22 00:57 96ee2a69

View on Github →

feat(order/filter/basic): prove @cofinite ℕ = at_top (#1888)

feat(order/filter/basic): prove @cofinite ℕ = at_top Also generalize not_injective_(nat/int)_fintype, and use [infinite α] instead of set.infinite (@univ α) as an argument.
Update src/data/equiv/basic.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
Drop a duplicate definition, thanks @ChrisHughes24

Estimated changes

Modified src/algebra/char_p.lean

Modified src/data/fintype.lean

added theorem not_injective_infinite_fintype

added theorem not_surjective_fintype_infinite

Modified src/data/real/hyperreal.lean

Modified src/data/set/finite.lean

added theorem set.infinite_univ

added theorem set.infinite_univ_iff

deleted theorem set.infinite_univ_nat

deleted theorem set.not_injective_int_fintype

deleted theorem set.not_injective_nat_fintype

Modified src/group_theory/order_of_element.lean

Modified src/order/filter/basic.lean

modified theorem filter.cofinite_ne_bot

modified theorem filter.compl_mem_hyperfilter_of_finite

added theorem filter.frequently_cofinite_iff_infinite

modified theorem filter.hyperfilter_le_cofinite

modified theorem filter.is_ultrafilter_hyperfilter

added theorem filter.mem_cofinite

modified theorem filter.mem_hyperfilter_of_finite_compl

modified theorem filter.nmem_hyperfilter_of_finite

added theorem nat.cofinite_eq_at_top

added theorem set.infinite_iff_frequently_cofinite