Commit 2023-01-23 08:16 caa949fb

View on Github →

Feat: port Order.Filter.Basic (#1750)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Logic/Function/Conjugate.lean

added theorem Function.Commute.semiconj

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Order/Filter/Basic.lean

added theorem Filter.Eventually.and_frequently

added theorem Filter.Eventually.choice

added theorem Filter.Eventually.comap

added theorem Filter.Eventually.congr

added theorem Filter.Eventually.exists

added theorem Filter.Eventually.exists_mem

added theorem Filter.Eventually.filter_mono

added theorem Filter.Eventually.frequently

added theorem Filter.Eventually.lt_top_iff_ne_top

added theorem Filter.Eventually.lt_top_of_ne

added theorem Filter.Eventually.mono

added theorem Filter.Eventually.mp

added theorem Filter.Eventually.ne_of_lt

added theorem Filter.Eventually.ne_top_of_lt

added theorem Filter.EventuallyEq.compl

added theorem Filter.EventuallyEq.comp₂

added theorem Filter.EventuallyEq.const_smul

added theorem Filter.EventuallyEq.diff

added theorem Filter.EventuallyEq.div

added theorem Filter.EventuallyEq.eventually

added theorem Filter.EventuallyEq.exists_mem

added theorem Filter.EventuallyEq.filter_mono

added theorem Filter.EventuallyEq.fun_comp

added theorem Filter.EventuallyEq.inf

added theorem Filter.EventuallyEq.inter

added theorem Filter.EventuallyEq.inv

added theorem Filter.EventuallyEq.le

added theorem Filter.EventuallyEq.mul

added theorem Filter.EventuallyEq.preimage

added theorem Filter.EventuallyEq.prod_mk

added theorem Filter.EventuallyEq.refl

added theorem Filter.EventuallyEq.rfl

added theorem Filter.EventuallyEq.rw

added theorem Filter.EventuallyEq.smul

added theorem Filter.EventuallyEq.sub_eq

added theorem Filter.EventuallyEq.sup

added theorem Filter.EventuallyEq.symm

added theorem Filter.EventuallyEq.trans

added theorem Filter.EventuallyEq.trans_le

added theorem Filter.EventuallyEq.union

added def Filter.EventuallyEq

added theorem Filter.EventuallyLe.antisymm

added theorem Filter.EventuallyLe.compl

added theorem Filter.EventuallyLe.congr

added theorem Filter.EventuallyLe.diff

added theorem Filter.EventuallyLe.inter

added theorem Filter.EventuallyLe.le_iff_eq

added theorem Filter.EventuallyLe.le_sup_of_le_left

added theorem Filter.EventuallyLe.le_sup_of_le_right

added theorem Filter.EventuallyLe.mul_le_mul'

added theorem Filter.EventuallyLe.mul_le_mul

added theorem Filter.EventuallyLe.mul_nonneg

added theorem Filter.EventuallyLe.refl

added theorem Filter.EventuallyLe.rfl

added theorem Filter.EventuallyLe.sup

added theorem Filter.EventuallyLe.sup_le

added theorem Filter.EventuallyLe.trans

added theorem Filter.EventuallyLe.trans_eq

added theorem Filter.EventuallyLe.union

added def Filter.EventuallyLe

added theorem Filter.Frequently.and_eventually

added theorem Filter.Frequently.exists

added theorem Filter.Frequently.filter_mono

added theorem Filter.Frequently.mono

added theorem Filter.Frequently.mp

added inductive Filter.GenerateSets

added theorem Filter.Iic_principal

added theorem Filter.NeBot.comap_of_image_mem

added theorem Filter.NeBot.comap_of_range_mem

added theorem Filter.NeBot.comap_of_surj

added theorem Filter.NeBot.map

added theorem Filter.NeBot.mono

added theorem Filter.NeBot.ne

added theorem Filter.NeBot.nonempty_of_mem

added theorem Filter.NeBot.not_disjoint

added theorem Filter.NeBot.of_map

added theorem Filter.Tendsto.comp

added theorem Filter.Tendsto.congr'

added theorem Filter.Tendsto.congr

added theorem Filter.Tendsto.eventually

added theorem Filter.Tendsto.frequently

added theorem Filter.Tendsto.frequently_map

added theorem Filter.Tendsto.if'

added theorem Filter.Tendsto.if

added theorem Filter.Tendsto.inf

added theorem Filter.Tendsto.mono_left

added theorem Filter.Tendsto.mono_right

added theorem Filter.Tendsto.neBot

added theorem Filter.Tendsto.not_tendsto

added theorem Filter.Tendsto.of_tendsto_comp

added theorem Filter.Tendsto.piecewise

added theorem Filter.Tendsto.sup

added def Filter.Tendsto

added def Filter.bind

added theorem Filter.bind_def

added theorem Filter.bind_inf_principal

added theorem Filter.bind_le

added theorem Filter.bind_mono

added theorem Filter.binfᵢ_sets_eq

added theorem Filter.binterᵢ_finset_mem

added theorem Filter.binterᵢ_mem

added theorem Filter.bot_sets_eq

added def Filter.comap

added theorem Filter.comap_bot

added theorem Filter.comap_coe_neBot_of_le_principal

added theorem Filter.comap_comap

added theorem Filter.comap_comm

added theorem Filter.comap_const_of_mem

added theorem Filter.comap_const_of_not_mem

added theorem Filter.comap_eq_bot_iff_compl_range

added theorem Filter.comap_eq_of_inverse

added theorem Filter.comap_equiv_symm

added theorem Filter.comap_eval_neBot

added theorem Filter.comap_eval_neBot_iff'

added theorem Filter.comap_eval_neBot_iff

added theorem Filter.comap_fst_neBot

added theorem Filter.comap_fst_neBot_iff

added theorem Filter.comap_id

added theorem Filter.comap_inf

added theorem Filter.comap_inf_principal_neBot_of_image_mem

added theorem Filter.comap_inf_principal_range

added theorem Filter.comap_infᵢ

added theorem Filter.comap_le_comap_iff

added theorem Filter.comap_map

added theorem Filter.comap_mono

added theorem Filter.comap_neBot

added theorem Filter.comap_neBot_iff

added theorem Filter.comap_neBot_iff_compl_range

added theorem Filter.comap_neBot_iff_frequently

added theorem Filter.comap_principal

added theorem Filter.comap_pure

added theorem Filter.comap_snd_neBot

added theorem Filter.comap_snd_neBot_iff

added theorem Filter.comap_sup

added theorem Filter.comap_supᵢ

added theorem Filter.comap_supₛ

added theorem Filter.comap_surjective_eq_bot

added theorem Filter.comap_top

added theorem Filter.compl_mem_comap

added theorem Filter.compl_not_mem

added theorem Filter.congr_sets

added theorem Filter.diff_mem

added theorem Filter.diff_mem_inf_principal_compl

added theorem Filter.disjoint_comap

added theorem Filter.disjoint_comap_iff

added theorem Filter.disjoint_map

added theorem Filter.disjoint_of_disjoint_of_mem

added theorem Filter.empty_mem_iff_bot

added theorem Filter.empty_not_mem

added theorem Filter.eq_binfᵢ_of_mem_iff_exists_mem

added theorem Filter.eq_infᵢ_of_mem_iff_exists_mem

added theorem Filter.eq_infₛ_of_mem_iff_exists_mem

added theorem Filter.eq_top_of_neBot

added theorem Filter.eventuallyEq_bind

added theorem Filter.eventuallyEq_empty

added theorem Filter.eventuallyEq_iff_exists_mem

added theorem Filter.eventuallyEq_iff_sub

added theorem Filter.eventuallyEq_inf_principal_iff

added theorem Filter.eventuallyEq_of_left_inv_of_right_inv

added theorem Filter.eventuallyEq_of_mem

added theorem Filter.eventuallyEq_principal

added theorem Filter.eventuallyEq_set

added theorem Filter.eventuallyEq_univ

added theorem Filter.eventuallyLe_antisymm_iff

added theorem Filter.eventuallyLe_bind

added theorem Filter.eventuallyLe_congr

added theorem Filter.eventually_all

added theorem Filter.eventually_all_finite

added theorem Filter.eventually_all_finset

added theorem Filter.eventually_and

added theorem Filter.eventually_bind

added theorem Filter.eventually_bot

added theorem Filter.eventually_comap

added theorem Filter.eventually_congr

added theorem Filter.eventually_const

added theorem Filter.eventually_false_iff_eq_bot

added theorem Filter.eventually_iff

added theorem Filter.eventually_iff_exists_mem

added theorem Filter.eventually_imp_distrib_left

added theorem Filter.eventually_imp_distrib_right

added theorem Filter.eventually_inf

added theorem Filter.eventually_inf_principal

added theorem Filter.eventually_map

added theorem Filter.eventually_mem_set

added theorem Filter.eventually_of_forall

added theorem Filter.eventually_of_mem

added theorem Filter.eventually_or_distrib_left

added theorem Filter.eventually_or_distrib_right

added theorem Filter.eventually_principal

added theorem Filter.eventually_pure

added theorem Filter.eventually_sub_nonneg

added theorem Filter.eventually_sup

added theorem Filter.eventually_supᵢ

added theorem Filter.eventually_supₛ

added theorem Filter.eventually_top

added theorem Filter.eventually_true

added theorem Filter.exists_interᵢ_of_mem_infᵢ

added theorem Filter.exists_mem_and_iff

added theorem Filter.exists_mem_subset_iff

added theorem Filter.filter_eq

added theorem Filter.filter_eq_bot_of_isEmpty

added theorem Filter.filter_eq_iff

added theorem Filter.forall_eventually_of_eventually_forall

added theorem Filter.forall_in_swap

added theorem Filter.forall_mem_nonempty_iff_neBot

added theorem Filter.frequently_and_distrib_left

added theorem Filter.frequently_and_distrib_right

added theorem Filter.frequently_bot

added theorem Filter.frequently_comap

added theorem Filter.frequently_const

added theorem Filter.frequently_false

added theorem Filter.frequently_iff

added theorem Filter.frequently_iff_forall_eventually_exists_and

added theorem Filter.frequently_imp_distrib

added theorem Filter.frequently_imp_distrib_left

added theorem Filter.frequently_imp_distrib_right

added theorem Filter.frequently_map

added theorem Filter.frequently_of_forall

added theorem Filter.frequently_or_distrib

added theorem Filter.frequently_or_distrib_left

added theorem Filter.frequently_or_distrib_right

added theorem Filter.frequently_principal

added theorem Filter.frequently_sup

added theorem Filter.frequently_supᵢ

added theorem Filter.frequently_supₛ

added theorem Filter.frequently_top

added theorem Filter.frequently_true_iff_neBot

added theorem Filter.gc_map_comap

added def Filter.generate

added theorem Filter.generate_empty

added theorem Filter.generate_eq_binfᵢ

added theorem Filter.generate_union

added theorem Filter.generate_unionᵢ

added theorem Filter.generate_univ

added def Filter.giGenerate

added theorem Filter.image_coe_mem_of_mem_comap

added theorem Filter.image_mem_map

added theorem Filter.image_mem_map_iff

added theorem Filter.image_mem_of_mem_comap

added theorem Filter.inf_eq_bot_iff

added theorem Filter.inf_principal

added theorem Filter.inf_principal_eq_bot

added theorem Filter.inf_principal_eq_bot_iff_comap

added theorem Filter.infᵢ_eq_generate

added theorem Filter.infᵢ_neBot_iff_of_directed'

added theorem Filter.infᵢ_neBot_iff_of_directed

added theorem Filter.infᵢ_neBot_of_directed'

added theorem Filter.infᵢ_neBot_of_directed

added theorem Filter.infᵢ_principal

added theorem Filter.infᵢ_principal_finite

added theorem Filter.infᵢ_principal_finset

added theorem Filter.infᵢ_sets_eq

added theorem Filter.infᵢ_sets_eq_finite'

added theorem Filter.infᵢ_sets_eq_finite

added theorem Filter.infᵢ_sets_induct

added theorem Filter.infₛ_neBot_of_directed'

added theorem Filter.infₛ_neBot_of_directed

added theorem Filter.inter_eventuallyEq_left

added theorem Filter.inter_eventuallyEq_right

added theorem Filter.inter_mem

added theorem Filter.inter_mem_iff

added theorem Filter.inter_mem_inf

added theorem Filter.interᵢ_mem

added theorem Filter.interₛ_comap_sets

added theorem Filter.interₛ_mem

added theorem Filter.isCompl_principal

added def Filter.join

added theorem Filter.join_le

added theorem Filter.join_mono

added theorem Filter.join_principal_eq_supₛ

added theorem Filter.join_pure

added theorem Filter.le_comap_map

added theorem Filter.le_comap_top

added theorem Filter.le_def

added theorem Filter.le_generate_iff

added theorem Filter.le_map

added theorem Filter.le_map_iff

added theorem Filter.le_map_of_right_inverse

added theorem Filter.le_principal_iff

added theorem Filter.le_pure_iff

added theorem Filter.le_seq

added def Filter.map

added theorem Filter.map_binfᵢ_eq

added theorem Filter.map_bot

added theorem Filter.map_comap

added theorem Filter.map_comap_le

added theorem Filter.map_comap_of_mem

added theorem Filter.map_comap_of_surjective

added theorem Filter.map_comm

added theorem Filter.map_compose

added theorem Filter.map_congr

added theorem Filter.map_const

added theorem Filter.map_def

added theorem Filter.map_eq_bot_iff

added theorem Filter.map_eq_comap_of_inverse

added theorem Filter.map_eq_map_iff_of_injOn

added theorem Filter.map_eq_of_inverse

added theorem Filter.map_equiv_symm

added theorem Filter.map_id'

added theorem Filter.map_id

added theorem Filter.map_inf'

added theorem Filter.map_inf

added theorem Filter.map_inf_le

added theorem Filter.map_inf_principal_preimage

added theorem Filter.map_infᵢ_eq

added theorem Filter.map_infᵢ_le

added theorem Filter.map_inj

added theorem Filter.map_injective

added theorem Filter.map_le_iff_le_comap

added theorem Filter.map_le_map_iff

added theorem Filter.map_le_map_iff_of_injOn

added theorem Filter.map_map

added theorem Filter.map_mono

added theorem Filter.map_neBot_iff

added theorem Filter.map_principal

added theorem Filter.map_pure

added theorem Filter.map_sup

added theorem Filter.map_supᵢ

added theorem Filter.map_swap4_eq_comap

added theorem Filter.map_swap_eq_comap_swap

added theorem Filter.map_top

added theorem Filter.mem_bind'

added theorem Filter.mem_bind

added theorem Filter.mem_binfᵢ_of_directed

added theorem Filter.mem_bot

added theorem Filter.mem_comap'

added theorem Filter.mem_comap

added theorem Filter.mem_comap_iff

added theorem Filter.mem_comap_iff_compl

added theorem Filter.mem_generate_iff

added theorem Filter.mem_inf_iff

added theorem Filter.mem_inf_iff_superset

added theorem Filter.mem_inf_of_inter

added theorem Filter.mem_inf_of_left

added theorem Filter.mem_inf_of_right

added theorem Filter.mem_inf_principal'

added theorem Filter.mem_inf_principal

added theorem Filter.mem_infᵢ'

added theorem Filter.mem_infᵢ

added theorem Filter.mem_infᵢ_finite'

added theorem Filter.mem_infᵢ_finite

added theorem Filter.mem_infᵢ_finset

added theorem Filter.mem_infᵢ_of_directed

added theorem Filter.mem_infᵢ_of_finite

added theorem Filter.mem_infᵢ_of_interᵢ

added theorem Filter.mem_infᵢ_of_mem

added theorem Filter.mem_join

added theorem Filter.mem_map'

added theorem Filter.mem_map

added theorem Filter.mem_map_iff_exists_image

added theorem Filter.mem_map_seq_iff

added theorem Filter.mem_of_eq_bot

added theorem Filter.mem_of_superset

added theorem Filter.mem_principal

added theorem Filter.mem_principal_self

added theorem Filter.mem_pure

added theorem Filter.mem_seq_def

added theorem Filter.mem_seq_iff

added theorem Filter.mem_sup

added theorem Filter.mem_supᵢ

added theorem Filter.mem_supₛ

added theorem Filter.mem_top

added theorem Filter.mem_top_iff_forall

added theorem Filter.mem_traverse

added theorem Filter.mem_traverse_iff

added theorem Filter.mkOfClosure_sets

added theorem Filter.monotone_mem

added theorem Filter.monotone_principal

added theorem Filter.mp_mem

added theorem Filter.neBot_iff

added theorem Filter.neBot_of_comap

added theorem Filter.neBot_of_le

added theorem Filter.nonempty_of_mem

added theorem Filter.nonempty_of_neBot

added theorem Filter.nontrivial_iff_nonempty

added theorem Filter.not_disjoint_self_iff

added theorem Filter.not_eventually

added theorem Filter.not_frequently

added theorem Filter.not_neBot

added theorem Filter.preimage_mem_comap

added def Filter.principal

added theorem Filter.principal_bind

added theorem Filter.principal_empty

added theorem Filter.principal_eq_bot_iff

added theorem Filter.principal_eq_iff_eq

added theorem Filter.principal_eq_map_coe_top

added theorem Filter.principal_le_iff

added theorem Filter.principal_mono

added theorem Filter.principal_neBot_iff

added theorem Filter.principal_singleton

added theorem Filter.principal_univ

added theorem Filter.prod_map_seq_comm

added theorem Filter.pure_bind

added theorem Filter.pure_injective

added theorem Filter.pure_le_iff

added theorem Filter.pure_seq_eq_map

added theorem Filter.pure_sets

added theorem Filter.range_mem_map

added def Filter.seq

added theorem Filter.seq_assoc

added theorem Filter.seq_eq_filter_seq

added theorem Filter.seq_mem_seq

added theorem Filter.seq_mono

added theorem Filter.seq_pure

added theorem Filter.sequence_mono

added theorem Filter.singleton_mem_pure

added theorem Filter.subtype_coe_map_comap

added theorem Filter.sup_bind

added theorem Filter.sup_join

added theorem Filter.sup_neBot

added theorem Filter.sup_principal

added theorem Filter.sup_sets_eq

added theorem Filter.supᵢ_inf_principal

added theorem Filter.supᵢ_join

added theorem Filter.supᵢ_neBot

added theorem Filter.supᵢ_principal

added theorem Filter.supᵢ_sets_eq

added theorem Filter.supₛ_sets_eq

added theorem Filter.tendsto_bot

added theorem Filter.tendsto_comap'_iff

added theorem Filter.tendsto_comap

added theorem Filter.tendsto_comap_iff

added theorem Filter.tendsto_congr'

added theorem Filter.tendsto_congr

added theorem Filter.tendsto_const_pure

added theorem Filter.tendsto_def

added theorem Filter.tendsto_id'

added theorem Filter.tendsto_id

added theorem Filter.tendsto_iff_comap

added theorem Filter.tendsto_iff_eventually

added theorem Filter.tendsto_inf

added theorem Filter.tendsto_inf_left

added theorem Filter.tendsto_inf_right

added theorem Filter.tendsto_infᵢ'

added theorem Filter.tendsto_infᵢ

added theorem Filter.tendsto_map'_iff

added theorem Filter.tendsto_map

added theorem Filter.tendsto_of_isEmpty

added theorem Filter.tendsto_principal

added theorem Filter.tendsto_principal_principal

added theorem Filter.tendsto_pure

added theorem Filter.tendsto_pure_left

added theorem Filter.tendsto_pure_pure

added theorem Filter.tendsto_sup

added theorem Filter.tendsto_supᵢ

added theorem Filter.tendsto_top

added theorem Filter.union_mem_sup

added theorem Filter.univ_mem'

added theorem Filter.univ_mem

added structure Filter

added theorem Function.Commute.filter_comap

added theorem Function.Commute.filter_map

added theorem Function.Semiconj.filter_comap

added theorem Function.Semiconj.filter_map

added theorem Function.Surjective.filter_map_top

added theorem HasSubset.Subset.eventuallyLe

added theorem Pairwise.exists_mem_filter_of_disjoint

added theorem Set.EqOn.eventuallyEq

added theorem Set.EqOn.eventuallyEq_of_mem

added theorem Set.MapsTo.tendsto

added theorem Set.PairwiseDisjoint.exists_mem_filter