Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 11:47 856cfd48

View on Github →

feat(order/liminf_limsup): define filter.blimsup, filter.bliminf (#16819) Also characterise cofinite.limsup and cofinite.liminf for the lattice of sets.

Estimated changes

modified theorem filter.Liminf_bot
modified theorem filter.Liminf_eq_supr_Inf
modified theorem filter.Liminf_top
modified theorem filter.Limsup_bot
modified theorem filter.Limsup_eq_infi_Sup
modified theorem filter.Limsup_top
added def filter.bliminf
added theorem filter.bliminf_eq
added theorem filter.bliminf_false
added theorem filter.bliminf_true
added def filter.blimsup
added theorem filter.blimsup_eq
added theorem filter.blimsup_false
added theorem filter.blimsup_mono
added theorem filter.blimsup_true
modified theorem filter.infi_le_liminf
modified def filter.liminf
modified theorem filter.liminf_const_top
modified theorem filter.liminf_eq
modified theorem filter.liminf_eq_supr_infi
modified def filter.limsup
modified theorem filter.limsup_const_bot
modified theorem filter.limsup_eq
modified theorem filter.limsup_eq_infi_supr
modified theorem filter.limsup_le_supr
added theorem filter.mono_bliminf'
added theorem filter.mono_bliminf
added theorem filter.mono_blimsup'
added theorem filter.mono_blimsup
modified theorem bsupr_limsup_dimH
modified theorem supr_limsup_dimH