Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-25 13:06 bf041275

View on Github →

feat(order): add liminf and limsup over filters (c.f. Sébastien Gouëzel's #115)

Estimated changes

Modified analysis/topology/topological_structures.lean

added theorem Liminf_eq_of_le_nhds

added theorem Liminf_nhds

added theorem Limsup_eq_of_le_nhds

added theorem Limsup_nhds

added theorem gt_mem_sets_of_Liminf_gt

added theorem is_bounded_ge_nhds

added theorem is_bounded_le_nhds

added theorem is_bounded_under_ge_of_tendsto

added theorem is_bounded_under_le_of_tendsto

added theorem is_cobounded_ge_nhds

added theorem is_cobounded_le_nhds

added theorem is_cobounded_under_ge_of_tendsto

added theorem is_cobounded_under_le_of_tendsto

added theorem le_nhds_of_Limsup_eq_Liminf

added theorem lt_mem_sets_of_Limsup_lt

Modified logic/basic.lean

added theorem exists_true_iff_nonempty

Modified order/conditionally_complete_lattice.lean

added theorem lattice.cInf_lower_bounds_eq_cSup

added theorem lattice.cSup_upper_bounds_eq_cInf

Modified order/lattice.lean

added theorem lattice.forall_le_or_exists_lt_inf

added theorem lattice.forall_le_or_exists_lt_sup

Created order/liminf_limsup.lean

added def filter.Liminf

added theorem filter.Liminf_bot

added theorem filter.Liminf_eq_supr_Inf

added theorem filter.Liminf_le_Liminf

added theorem filter.Liminf_le_Liminf_of_le

added theorem filter.Liminf_le_Limsup

added theorem filter.Liminf_le_of_le

added theorem filter.Liminf_principal

added theorem filter.Liminf_top

added def filter.Limsup

added theorem filter.Limsup_bot

added theorem filter.Limsup_eq_infi_Sup

added theorem filter.Limsup_le_Limsup

added theorem filter.Limsup_le_Limsup_of_le

added theorem filter.Limsup_le_of_le

added theorem filter.Limsup_principal

added theorem filter.Limsup_top

added def filter.is_bounded

added theorem filter.is_bounded_bot

added theorem filter.is_bounded_ge_of_bot

added theorem filter.is_bounded_iff

added theorem filter.is_bounded_le_of_top

added theorem filter.is_bounded_of_le

added theorem filter.is_bounded_principal

added theorem filter.is_bounded_sup

added theorem filter.is_bounded_top

added def filter.is_bounded_under

added theorem filter.is_bounded_under_inf

added theorem filter.is_bounded_under_of

added theorem filter.is_bounded_under_of_is_bounded

added theorem filter.is_bounded_under_sup

added theorem filter.is_cobounded.mk

added def filter.is_cobounded

added theorem filter.is_cobounded_bot

added theorem filter.is_cobounded_ge_of_top

added theorem filter.is_cobounded_le_of_bot

added theorem filter.is_cobounded_of_is_bounded

added theorem filter.is_cobounded_of_le

added theorem filter.is_cobounded_principal

added theorem filter.is_cobounded_top

added def filter.is_cobounded_under

added theorem filter.le_Liminf_of_le

added theorem filter.le_Limsup_of_le

added def filter.liminf

added theorem filter.liminf_eq

added theorem filter.liminf_eq_supr_infi

added theorem filter.liminf_le_liminf

added def filter.limsup

added theorem filter.limsup_eq

added theorem filter.limsup_eq_infi_supr

added theorem filter.limsup_le_limsup