Commit 2023-01-24 07:05 8992742d

View on Github →

feat: port Order.Filter.CountableInter (#1803)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/CountableInter.lean

added theorem EventuallyEq.countable_bInter

added theorem EventuallyEq.countable_bUnion

added theorem EventuallyEq.countable_interᵢ

added theorem EventuallyEq.countable_unionᵢ

added theorem EventuallyLe.countable_bInter

added theorem EventuallyLe.countable_bUnion

added theorem EventuallyLe.countable_interᵢ

added theorem EventuallyLe.countable_unionᵢ

added theorem Filter.mem_ofCountableInter

added def Filter.ofCountableInter

added theorem countable_bInter_mem

added theorem countable_interᵢ_mem

added theorem countable_interₛ_mem

added theorem eventually_countable_ball

added theorem eventually_countable_forall