Commit 2023-01-24 09:14 cea40ebd

View on Github →

feat: port Order.Filter.AtTopBot (#1795)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem cinfᵢ_subsingleton

added theorem csupᵢ_subsingleton

Created Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.Eventually.exists_forall_of_atBot

added theorem Filter.Eventually.exists_forall_of_atTop

added theorem Filter.Frequently.forall_exists_of_atBot

added theorem Filter.Frequently.forall_exists_of_atTop

added theorem Filter.HasAntitoneBasis.comp_mono

added theorem Filter.HasAntitoneBasis.comp_strictMono

added theorem Filter.HasAntitoneBasis.eventually_subset

added theorem Filter.HasAntitoneBasis.subbasis_with_rel

added theorem Filter.Ici_mem_atTop

added theorem Filter.Iic_mem_atBot

added theorem Filter.Iio_mem_atBot

added theorem Filter.Ioi_mem_atTop

added theorem Filter.OrderBot.atBot_eq

added theorem Filter.OrderTop.atTop_eq

added theorem Filter.Subsingleton.atBot_eq

added theorem Filter.Subsingleton.atTop_eq

added theorem Filter.Tendsto.atBot_div_const

added theorem Filter.Tendsto.atBot_mul_atBot

added theorem Filter.Tendsto.atBot_mul_atTop

added theorem Filter.Tendsto.atBot_mul_const

added theorem Filter.Tendsto.atBot_mul_neg_const

added theorem Filter.Tendsto.atTop_div_const

added theorem Filter.Tendsto.atTop_mul_atBot

added theorem Filter.Tendsto.atTop_mul_atTop

added theorem Filter.Tendsto.atTop_mul_const

added theorem Filter.Tendsto.atTop_mul_neg_const

added theorem Filter.Tendsto.atTop_of_const_mul

added theorem Filter.Tendsto.atTop_of_mul_const

added theorem Filter.Tendsto.const_mul_atBot

added theorem Filter.Tendsto.const_mul_atTop

added theorem Filter.Tendsto.neg_const_mul_atBot

added theorem Filter.Tendsto.neg_const_mul_atTop

added theorem Filter.Tendsto.nsmul_atBot

added theorem Filter.Tendsto.nsmul_atTop

added theorem Filter.Tendsto.prod_atBot

added theorem Filter.Tendsto.prod_atTop

added theorem Filter.Tendsto.prod_map_prod_atBot

added theorem Filter.Tendsto.prod_map_prod_atTop

added theorem Filter.Tendsto.subseq_mem

added def Filter.atBot

added theorem Filter.atBot_Iic_eq

added theorem Filter.atBot_Iio_eq

added theorem Filter.atBot_basis'

added theorem Filter.atBot_basis

added theorem Filter.atBot_countable_basis

added theorem Filter.atBot_neBot

added def Filter.atTop

added theorem Filter.atTop_Ici_eq

added theorem Filter.atTop_Ioi_eq

added theorem Filter.atTop_basis'

added theorem Filter.atTop_basis

added theorem Filter.atTop_basis_Ioi

added theorem Filter.atTop_countable_basis

added theorem Filter.atTop_finset_eq_infᵢ

added theorem Filter.atTop_neBot

added theorem Filter.comap_abs_atTop

added theorem Filter.comap_embedding_atBot

added theorem Filter.comap_embedding_atTop

added theorem Filter.comap_neg_atBot

added theorem Filter.comap_neg_atTop

added theorem Filter.disjoint_atBot_atTop

added theorem Filter.disjoint_atBot_principal_Ici

added theorem Filter.disjoint_atBot_principal_Ioi

added theorem Filter.disjoint_atTop_atBot

added theorem Filter.disjoint_atTop_principal_Iic

added theorem Filter.disjoint_atTop_principal_Iio

added theorem Filter.disjoint_pure_atBot

added theorem Filter.disjoint_pure_atTop

added theorem Filter.eventually_atBot

added theorem Filter.eventually_atBot_curry

added theorem Filter.eventually_atBot_prod_self'

added theorem Filter.eventually_atBot_prod_self

added theorem Filter.eventually_atTop

added theorem Filter.eventually_atTop_curry

added theorem Filter.eventually_atTop_prod_self'

added theorem Filter.eventually_atTop_prod_self

added theorem Filter.eventually_ge_atTop

added theorem Filter.eventually_gt_atTop

added theorem Filter.eventually_iff_seq_eventually

added theorem Filter.eventually_le_atBot

added theorem Filter.eventually_lt_atBot

added theorem Filter.eventually_ne_atBot

added theorem Filter.eventually_ne_atTop

added theorem Filter.exists_le_of_tendsto_atBot

added theorem Filter.exists_le_of_tendsto_atTop

added theorem Filter.exists_lt_of_tendsto_atBot

added theorem Filter.exists_lt_of_tendsto_atTop

added theorem Filter.exists_seq_forall_of_frequently

added theorem Filter.exists_seq_tendsto

added theorem Filter.extraction_forall_of_eventually'

added theorem Filter.extraction_forall_of_eventually

added theorem Filter.extraction_forall_of_frequently

added theorem Filter.extraction_of_eventually_atTop

added theorem Filter.extraction_of_frequently_atTop'

added theorem Filter.extraction_of_frequently_atTop

added theorem Filter.frequently_atBot'

added theorem Filter.frequently_atBot

added theorem Filter.frequently_atTop'

added theorem Filter.frequently_atTop

added theorem Filter.frequently_high_scores

added theorem Filter.frequently_iff_seq_frequently

added theorem Filter.frequently_low_scores

added theorem Filter.high_scores

added theorem Filter.inf_map_atBot_neBot_iff

added theorem Filter.inf_map_atTop_neBot_iff

added theorem Filter.low_scores

added theorem Filter.map_add_atTop_eq_nat

added theorem Filter.map_atBot_eq

added theorem Filter.map_atBot_eq_of_gc

added theorem Filter.map_atTop_eq

added theorem Filter.map_atTop_eq_of_gc

added theorem Filter.map_atTop_finset_prod_le_of_prod_eq

added theorem Filter.map_div_atTop_eq_nat

added theorem Filter.map_neg_atBot

added theorem Filter.map_neg_atTop

added theorem Filter.map_sub_atTop_eq_nat

added theorem Filter.map_val_Ici_atTop

added theorem Filter.map_val_Iic_atBot

added theorem Filter.map_val_Iio_atBot

added theorem Filter.map_val_Ioi_atTop

added theorem Filter.map_val_atTop_of_Ici_subset

added theorem Filter.mem_atBot

added theorem Filter.mem_atBot_sets

added theorem Filter.mem_atTop

added theorem Filter.mem_atTop_sets

added theorem Filter.nonneg_of_eventually_pow_nonneg

added theorem Filter.not_tendsto_const_atBot

added theorem Filter.not_tendsto_const_atTop

added theorem Filter.not_tendsto_iff_exists_frequently_nmem

added theorem Filter.not_tendsto_pow_atTop_atBot

added theorem Filter.prod_atBot_atBot_eq

added theorem Filter.prod_atTop_atTop_eq

added theorem Filter.prod_map_atBot_eq

added theorem Filter.prod_map_atTop_eq

added theorem Filter.strictMono_subseq_of_id_le

added theorem Filter.strictMono_subseq_of_tendsto_atTop

added theorem Filter.subseq_forall_of_frequently

added theorem Filter.subseq_tendsto_of_neBot

added theorem Filter.tendsto_Ici_atTop

added theorem Filter.tendsto_Iic_atBot

added theorem Filter.tendsto_Iio_atBot

added theorem Filter.tendsto_Ioi_atTop

added theorem Filter.tendsto_abs_atBot_atTop

added theorem Filter.tendsto_abs_atTop_atTop

added theorem Filter.tendsto_add_atTop_iff_nat

added theorem Filter.tendsto_add_atTop_nat

added theorem Filter.tendsto_atBot'

added theorem Filter.tendsto_atBot

added theorem Filter.tendsto_atBot_add

added theorem Filter.tendsto_atBot_add_const_left

added theorem Filter.tendsto_atBot_add_const_right

added theorem Filter.tendsto_atBot_add_left_of_ge'

added theorem Filter.tendsto_atBot_add_left_of_ge

added theorem Filter.tendsto_atBot_add_nonpos_left'

added theorem Filter.tendsto_atBot_add_nonpos_left

added theorem Filter.tendsto_atBot_add_nonpos_right'

added theorem Filter.tendsto_atBot_add_nonpos_right

added theorem Filter.tendsto_atBot_add_right_of_ge'

added theorem Filter.tendsto_atBot_add_right_of_ge

added theorem Filter.tendsto_atBot_atBot

added theorem Filter.tendsto_atBot_atBot_iff_of_monotone

added theorem Filter.tendsto_atBot_atBot_of_monotone'

added theorem Filter.tendsto_atBot_atBot_of_monotone

added theorem Filter.tendsto_atBot_atTop

added theorem Filter.tendsto_atBot_diagonal

added theorem Filter.tendsto_atBot_embedding

added theorem Filter.tendsto_atBot_mono'

added theorem Filter.tendsto_atBot_mono

added theorem Filter.tendsto_atBot_of_add_bdd_below_left'

added theorem Filter.tendsto_atBot_of_add_bdd_below_left

added theorem Filter.tendsto_atBot_of_add_bdd_below_right'

added theorem Filter.tendsto_atBot_of_add_bdd_below_right

added theorem Filter.tendsto_atBot_of_add_const_left

added theorem Filter.tendsto_atBot_of_add_const_right

added theorem Filter.tendsto_atBot_of_monotone_of_filter

added theorem Filter.tendsto_atBot_of_monotone_of_subseq

added theorem Filter.tendsto_atBot_principal

added theorem Filter.tendsto_atBot_pure

added theorem Filter.tendsto_atTop'

added theorem Filter.tendsto_atTop

added theorem Filter.tendsto_atTop_add

added theorem Filter.tendsto_atTop_add_const_left

added theorem Filter.tendsto_atTop_add_const_right

added theorem Filter.tendsto_atTop_add_left_of_le'

added theorem Filter.tendsto_atTop_add_left_of_le

added theorem Filter.tendsto_atTop_add_nonneg_left'

added theorem Filter.tendsto_atTop_add_nonneg_left

added theorem Filter.tendsto_atTop_add_nonneg_right'

added theorem Filter.tendsto_atTop_add_nonneg_right

added theorem Filter.tendsto_atTop_add_right_of_le'

added theorem Filter.tendsto_atTop_add_right_of_le

added theorem Filter.tendsto_atTop_atBot

added theorem Filter.tendsto_atTop_atTop

added theorem Filter.tendsto_atTop_atTop_iff_of_monotone

added theorem Filter.tendsto_atTop_atTop_of_monotone'

added theorem Filter.tendsto_atTop_atTop_of_monotone

added theorem Filter.tendsto_atTop_diagonal

added theorem Filter.tendsto_atTop_embedding

added theorem Filter.tendsto_atTop_finset_of_monotone

added theorem Filter.tendsto_atTop_mono'

added theorem Filter.tendsto_atTop_mono

added theorem Filter.tendsto_atTop_of_add_bdd_above_left'

added theorem Filter.tendsto_atTop_of_add_bdd_above_left

added theorem Filter.tendsto_atTop_of_add_bdd_above_right'

added theorem Filter.tendsto_atTop_of_add_bdd_above_right

added theorem Filter.tendsto_atTop_of_add_const_left

added theorem Filter.tendsto_atTop_of_add_const_right

added theorem Filter.tendsto_atTop_of_monotone_of_filter

added theorem Filter.tendsto_atTop_of_monotone_of_subseq

added theorem Filter.tendsto_atTop_principal

added theorem Filter.tendsto_atTop_pure

added theorem Filter.tendsto_bit0_atBot

added theorem Filter.tendsto_bit0_atTop

added theorem Filter.tendsto_bit1_atTop

added theorem Filter.tendsto_comp_val_Ici_atTop

added theorem Filter.tendsto_comp_val_Iic_atBot

added theorem Filter.tendsto_comp_val_Iio_atBot

added theorem Filter.tendsto_comp_val_Ioi_atTop

added theorem Filter.tendsto_const_mul_atBot_iff

added theorem Filter.tendsto_const_mul_atBot_iff_neg

added theorem Filter.tendsto_const_mul_atBot_iff_pos

added theorem Filter.tendsto_const_mul_atBot_of_neg

added theorem Filter.tendsto_const_mul_atBot_of_pos

added theorem Filter.tendsto_const_mul_atTop_iff

added theorem Filter.tendsto_const_mul_atTop_iff_neg

added theorem Filter.tendsto_const_mul_atTop_iff_pos

added theorem Filter.tendsto_const_mul_atTop_of_neg

added theorem Filter.tendsto_const_mul_atTop_of_pos

added theorem Filter.tendsto_const_mul_pow_atBot_iff

added theorem Filter.tendsto_const_mul_pow_atTop

added theorem Filter.tendsto_const_mul_pow_atTop_iff

added theorem Filter.tendsto_finset_image_atTop_atTop

added theorem Filter.tendsto_finset_preimage_atTop_atTop

added theorem Filter.tendsto_finset_range

added theorem Filter.tendsto_iff_forall_eventually_mem

added theorem Filter.tendsto_iff_seq_tendsto

added theorem Filter.tendsto_mul_const_atBot_iff

added theorem Filter.tendsto_mul_const_atBot_iff_neg

added theorem Filter.tendsto_mul_const_atBot_iff_pos

added theorem Filter.tendsto_mul_const_atBot_of_neg

added theorem Filter.tendsto_mul_const_atBot_of_pos

added theorem Filter.tendsto_mul_const_atTop_iff

added theorem Filter.tendsto_mul_const_atTop_iff_neg

added theorem Filter.tendsto_mul_const_atTop_iff_pos

added theorem Filter.tendsto_mul_const_atTop_of_neg

added theorem Filter.tendsto_mul_const_atTop_of_pos

added theorem Filter.tendsto_mul_self_atTop

added theorem Filter.tendsto_neg_atBot_atTop

added theorem Filter.tendsto_neg_atBot_iff

added theorem Filter.tendsto_neg_atTop_atBot

added theorem Filter.tendsto_neg_atTop_iff

added theorem Filter.tendsto_neg_const_mul_pow_atTop

added theorem Filter.tendsto_of_seq_tendsto

added theorem Filter.tendsto_of_subseq_tendsto

added theorem Filter.tendsto_pow_atTop

added theorem Filter.tendsto_pow_atTop_iff

added theorem Filter.tendsto_sub_atTop_nat

added theorem Filter.unbounded_of_tendsto_atBot'

added theorem Filter.unbounded_of_tendsto_atBot

added theorem Filter.unbounded_of_tendsto_atTop'

added theorem Filter.unbounded_of_tendsto_atTop

added theorem Filter.zero_pow_eventuallyEq

added theorem Function.Injective.map_atTop_finset_prod_eq

added theorem OrderIso.comap_atBot

added theorem OrderIso.comap_atTop

added theorem OrderIso.map_atBot

added theorem OrderIso.map_atTop

added theorem OrderIso.tendsto_atBot

added theorem OrderIso.tendsto_atBot_iff

added theorem OrderIso.tendsto_atTop

added theorem OrderIso.tendsto_atTop_iff

added theorem StrictMono.tendsto_atTop

added theorem exists_le_mul_self

added theorem exists_lt_mul_self