Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-18 08:40 a5347cb9

View on Github →

feat(*): add various order-related lemmas (#16918) These all came up while preparing to introduce the definition of ergodic maps but it seems better to PR them separately.

Estimated changes

added theorem set.preimage_comp_eq
modified theorem set.preimage_id
added theorem set.preimage_id_eq
added theorem binfi_const
modified theorem binfi_inf
added theorem bsupr_const
added theorem bsupr_sup
modified theorem inf_binfi
added theorem infi_nat_gt_zero_eq
added theorem sup_bsupr
added theorem supr_nat_gt_zero_eq
added theorem filter.inf_liminf
added theorem filter.inf_limsup
added theorem filter.liminf_compl
added theorem filter.liminf_sdiff
added theorem filter.limsup_compl
added theorem filter.limsup_sdiff
added theorem filter.sdiff_liminf
added theorem filter.sdiff_limsup
added theorem filter.sup_liminf
added theorem filter.sup_limsup