Commit 2023-02-07 14:12 7a7c6e0d

View on Github →

feat: port Order.LiminfLimsup (#2078) Most notable parts of this file:

Needed to translate isBoundedDefault macro to lean4, very easy
Had to replace e with FunLike.coe e in a theorem statement to prevent strange coercion behaviour for Equivs.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/LiminfLimsup.lean

added theorem Antitone.isBoundedUnder_ge_comp

added theorem Antitone.isBoundedUnder_le_comp

added theorem Filter.CompleteLatticeHom.apply_liminf_iterate

added theorem Filter.CompleteLatticeHom.apply_limsup_iterate

added theorem Filter.HasBasis.liminf_eq_supᵢ_infᵢ

added theorem Filter.HasBasis.liminfₛ_eq_supᵢ_infₛ

added theorem Filter.HasBasis.limsup_eq_infᵢ_supᵢ

added theorem Filter.HasBasis.limsupₛ_eq_infᵢ_supₛ

added theorem Filter.InfHom.le_apply_bliminf

added theorem Filter.IsBounded.isBoundedUnder

added theorem Filter.IsBounded.isCobounded_flip

added theorem Filter.IsBounded.isCobounded_ge

added theorem Filter.IsBounded.isCobounded_le

added theorem Filter.IsBounded.mono

added def Filter.IsBounded

added theorem Filter.IsBoundedUnder.bddAbove_range

added theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite

added theorem Filter.IsBoundedUnder.bddBelow_range

added theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite

added theorem Filter.IsBoundedUnder.inf

added theorem Filter.IsBoundedUnder.mono

added theorem Filter.IsBoundedUnder.mono_ge

added theorem Filter.IsBoundedUnder.mono_le

added theorem Filter.IsBoundedUnder.sup

added def Filter.IsBoundedUnder

added theorem Filter.IsCobounded.mk

added theorem Filter.IsCobounded.mono

added def Filter.IsCobounded

added def Filter.IsCoboundedUnder

added theorem Filter.OrderIso.apply_bliminf

added theorem Filter.OrderIso.apply_blimsup

added theorem Filter.SupHom.apply_blimsup_le

added def Filter.bliminf

added theorem Filter.bliminf_antitone

added theorem Filter.bliminf_antitone_filter

added theorem Filter.bliminf_congr'

added theorem Filter.bliminf_congr

added theorem Filter.bliminf_eq

added theorem Filter.bliminf_eq_liminf_subtype

added theorem Filter.bliminf_eq_supᵢ_binfᵢ

added theorem Filter.bliminf_eq_supᵢ_binfᵢ_of_nat

added theorem Filter.bliminf_false

added theorem Filter.bliminf_or_eq_inf

added theorem Filter.bliminf_or_le_inf

added theorem Filter.bliminf_or_le_inf_aux_left

added theorem Filter.bliminf_or_le_inf_aux_right

added theorem Filter.bliminf_sup_le_and

added theorem Filter.bliminf_sup_le_and_aux_left

added theorem Filter.bliminf_sup_le_and_aux_right

added theorem Filter.bliminf_sup_le_inf_aux_left

added theorem Filter.bliminf_sup_le_inf_aux_right

added theorem Filter.bliminf_sup_le_or_aux_left

added theorem Filter.bliminf_sup_le_or_aux_right

added theorem Filter.bliminf_true

added def Filter.blimsup

added theorem Filter.blimsup_and_le_inf

added theorem Filter.blimsup_congr'

added theorem Filter.blimsup_congr

added theorem Filter.blimsup_eq

added theorem Filter.blimsup_eq_infᵢ_bsupᵢ

added theorem Filter.blimsup_eq_infᵢ_bsupᵢ_of_nat

added theorem Filter.blimsup_eq_limsup_subtype

added theorem Filter.blimsup_false

added theorem Filter.blimsup_mono

added theorem Filter.blimsup_monotone_filter

added theorem Filter.blimsup_or_eq_sup

added theorem Filter.blimsup_sup_le_or

added theorem Filter.blimsup_true

added theorem Filter.cofinite.bliminf_set_eq

added theorem Filter.cofinite.blimsup_set_eq

added theorem Filter.cofinite.liminf_set_eq

added theorem Filter.cofinite.limsup_set_eq

added theorem Filter.eventually_lt_of_limsup_lt

added theorem Filter.eventually_lt_of_lt_liminf

added theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup'

added theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup

added theorem Filter.frequently_lt_of_liminf_lt

added theorem Filter.frequently_lt_of_liminfₛ_lt

added theorem Filter.frequently_lt_of_lt_limsup

added theorem Filter.frequently_lt_of_lt_limsupₛ

added theorem Filter.inf_liminf

added theorem Filter.inf_limsup

added theorem Filter.infᵢ_le_liminf

added theorem Filter.isBoundedUnder_const

added theorem Filter.isBoundedUnder_ge_inf

added theorem Filter.isBoundedUnder_ge_inv

added theorem Filter.isBoundedUnder_le_abs

added theorem Filter.isBoundedUnder_le_inv

added theorem Filter.isBoundedUnder_le_sup

added theorem Filter.isBoundedUnder_of

added theorem Filter.isBounded_bot

added theorem Filter.isBounded_ge_of_bot

added theorem Filter.isBounded_iff

added theorem Filter.isBounded_le_of_top

added theorem Filter.isBounded_principal

added theorem Filter.isBounded_sup

added theorem Filter.isBounded_top

added theorem Filter.isCobounded_bot

added theorem Filter.isCobounded_ge_of_top

added theorem Filter.isCobounded_le_of_bot

added theorem Filter.isCobounded_principal

added theorem Filter.isCobounded_top

added theorem Filter.le_liminf_of_le

added theorem Filter.le_liminfₛ_of_le

added theorem Filter.le_limsup_of_frequently_le'

added theorem Filter.le_limsup_of_frequently_le

added theorem Filter.le_limsup_of_le

added theorem Filter.le_limsupₛ_of_le

added def Filter.liminf

added theorem Filter.liminf_compl

added theorem Filter.liminf_congr

added theorem Filter.liminf_const

added theorem Filter.liminf_const_top

added theorem Filter.liminf_eq

added theorem Filter.liminf_eq_supᵢ_infᵢ

added theorem Filter.liminf_eq_supᵢ_infᵢ_of_nat'

added theorem Filter.liminf_eq_supᵢ_infᵢ_of_nat

added theorem Filter.liminf_eq_supₛ_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_frequently_le'

added theorem Filter.liminf_le_of_frequently_le

added theorem Filter.liminf_le_of_le

added theorem Filter.liminf_nat_add

added theorem Filter.liminf_sdiff

added def Filter.liminfₛ

added theorem Filter.liminfₛ_bot

added theorem Filter.liminfₛ_eq_supᵢ_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_compl

added theorem Filter.limsup_congr

added theorem Filter.limsup_const

added theorem Filter.limsup_const_bot

added theorem Filter.limsup_eq

added theorem Filter.limsup_eq_infᵢ_supᵢ

added theorem Filter.limsup_eq_infᵢ_supᵢ_of_nat'

added theorem Filter.limsup_eq_infᵢ_supᵢ_of_nat

added theorem Filter.limsup_eq_infₛ_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_le_supᵢ

added theorem Filter.limsup_nat_add

added theorem Filter.limsup_sdiff

added def Filter.limsupₛ

added theorem Filter.limsupₛ_bot

added theorem Filter.limsupₛ_eq_infᵢ_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 theorem Filter.mono_bliminf'

added theorem Filter.mono_bliminf

added theorem Filter.mono_blimsup'

added theorem Filter.mono_blimsup

added theorem Filter.not_isBoundedUnder_of_tendsto_atBot

added theorem Filter.not_isBoundedUnder_of_tendsto_atTop

added theorem Filter.sdiff_liminf

added theorem Filter.sdiff_limsup

added theorem Filter.sup_liminf

added theorem Filter.sup_limsup

added theorem GaloisConnection.l_limsup_le

added theorem Monotone.isBoundedUnder_ge_comp

added theorem Monotone.isBoundedUnder_le_comp

added theorem OrderIso.isBoundedUnder_ge_comp

added theorem OrderIso.isBoundedUnder_le_comp

added theorem OrderIso.liminf_apply

added theorem OrderIso.limsup_apply