Commit 2023-01-24 07:28 218a453d

View on Github →

Feat: port Order.Filter.Bases (#1791)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Bases.lean

added theorem Disjoint.exists_mem_filter_basis

added structure Filter.CountableFilterBasis

added def Filter.FilterBasis.ofSets

added theorem Filter.FilterBasis.ofSets_sets

added theorem Filter.HasAntitoneBasis.hasBasis_ge

added theorem Filter.HasAntitoneBasis.map

added theorem Filter.HasAntitoneBasis.prod

added structure Filter.HasAntitoneBasis

added theorem Filter.HasBasis.comap

added theorem Filter.HasBasis.comp_equiv

added theorem Filter.HasBasis.comp_of_surjective

added theorem Filter.HasBasis.coprod

added theorem Filter.HasBasis.disjoint_iff

added theorem Filter.HasBasis.disjoint_iff_left

added theorem Filter.HasBasis.disjoint_iff_right

added theorem Filter.HasBasis.eq_binfᵢ

added theorem Filter.HasBasis.eq_bot_iff

added theorem Filter.HasBasis.eq_generate

added theorem Filter.HasBasis.eq_infᵢ

added theorem Filter.HasBasis.eq_of_same_basis

added theorem Filter.HasBasis.eventually_iff

added theorem Filter.HasBasis.ex_mem

added theorem Filter.HasBasis.exists_antitone_subbasis

added theorem Filter.HasBasis.exists_iff

added theorem Filter.HasBasis.ext

added theorem Filter.HasBasis.filter_eq

added theorem Filter.HasBasis.forall_iff

added theorem Filter.HasBasis.forall_mem_mem

added theorem Filter.HasBasis.frequently_iff

added theorem Filter.HasBasis.ge_iff

added theorem Filter.HasBasis.hasBasis_self_subset

added theorem Filter.HasBasis.inf'

added theorem Filter.HasBasis.inf

added theorem Filter.HasBasis.inf_basis_neBot_iff

added theorem Filter.HasBasis.inf_neBot_iff

added theorem Filter.HasBasis.inf_principal

added theorem Filter.HasBasis.inf_principal_neBot_iff

added theorem Filter.HasBasis.interₛ_sets

added theorem Filter.HasBasis.isBasis

added theorem Filter.HasBasis.le_basis_iff

added theorem Filter.HasBasis.le_iff

added theorem Filter.HasBasis.map

added theorem Filter.HasBasis.mem_iff

added theorem Filter.HasBasis.mem_of_mem

added theorem Filter.HasBasis.principal_inf

added theorem Filter.HasBasis.prod

added theorem Filter.HasBasis.prod_pprod

added theorem Filter.HasBasis.prod_same_index

added theorem Filter.HasBasis.prod_same_index_anti

added theorem Filter.HasBasis.prod_same_index_mono

added theorem Filter.HasBasis.prod_self

added theorem Filter.HasBasis.property_index

added theorem Filter.HasBasis.restrict

added theorem Filter.HasBasis.restrict_subset

added theorem Filter.HasBasis.set_index_mem

added theorem Filter.HasBasis.set_index_subset

added theorem Filter.HasBasis.sup'

added theorem Filter.HasBasis.sup

added theorem Filter.HasBasis.sup_principal

added theorem Filter.HasBasis.sup_pure

added theorem Filter.HasBasis.tendsto_iff

added theorem Filter.HasBasis.tendsto_left_iff

added theorem Filter.HasBasis.tendsto_right_iff

added theorem Filter.HasBasis.to_hasBasis

added theorem Filter.HasBasis.to_has_basis'

added theorem Filter.HasBasis.to_subset

added structure Filter.HasBasis

added theorem Filter.HasCountableBasis.isCountablyGenerated

added structure Filter.HasCountableBasis

added structure Filter.IsAntitoneBasis

added theorem Filter.IsBasis.filter_eq_generate

added theorem Filter.IsBasis.mem_filterBasis_iff

added structure Filter.IsBasis

added structure Filter.IsCountableBasis

added theorem Filter.Tendsto.basis_both

added theorem Filter.Tendsto.basis_left

added theorem Filter.Tendsto.basis_right

added theorem Filter.antitone_seq_of_seq

added def Filter.asBasis

added theorem Filter.asBasis_filter

added theorem Filter.basis_sets

added theorem Filter.comap_hasBasis

added theorem Filter.compl_diagonal_mem_prod

added theorem Filter.countable_binfᵢ_eq_infᵢ_seq'

added theorem Filter.countable_binfᵢ_eq_infᵢ_seq

added theorem Filter.countable_binfᵢ_principal_eq_seq_infᵢ

added theorem Filter.disjoint_principal_left

added theorem Filter.disjoint_principal_principal

added theorem Filter.disjoint_principal_right

added theorem Filter.disjoint_pure_pure

added theorem Filter.exists_antitone_basis

added theorem Filter.exists_antitone_seq

added theorem Filter.generate_eq_generate_inter

added theorem Filter.generate_neBot_iff

added theorem Filter.hasBasis_binfᵢ_of_directed'

added theorem Filter.hasBasis_binfᵢ_of_directed

added theorem Filter.hasBasis_binfᵢ_principal'

added theorem Filter.hasBasis_binfᵢ_principal

added theorem Filter.hasBasis_generate

added theorem Filter.hasBasis_iff

added theorem Filter.hasBasis_infᵢ'

added theorem Filter.hasBasis_infᵢ

added theorem Filter.hasBasis_infᵢ_of_directed'

added theorem Filter.hasBasis_infᵢ_of_directed

added theorem Filter.hasBasis_infᵢ_principal

added theorem Filter.hasBasis_infᵢ_principal_finite

added theorem Filter.hasBasis_principal

added theorem Filter.hasBasis_pure

added theorem Filter.hasBasis_self

added theorem Filter.hasBasis_supᵢ

added theorem Filter.inf_neBot_iff

added theorem Filter.inf_neBot_iff_frequently_left

added theorem Filter.inf_neBot_iff_frequently_right

added theorem Filter.inf_principal_neBot_iff

added theorem Filter.isCountablyGenerated_binfᵢ_principal

added theorem Filter.isCountablyGenerated_bot

added theorem Filter.isCountablyGenerated_iff_exists_antitone_basis

added theorem Filter.isCountablyGenerated_of_seq

added theorem Filter.isCountablyGenerated_principal

added theorem Filter.isCountablyGenerated_pure

added theorem Filter.isCountablyGenerated_seq

added theorem Filter.isCountablyGenerated_top

added theorem Filter.le_iff_forall_inf_principal_compl

added theorem Filter.map_sigma_mk_comap

added theorem Filter.mem_iff_inf_principal_compl

added theorem Filter.mem_prod_self_iff

added theorem Filter.not_mem_iff_inf_principal_compl

added theorem Filter.ofSets_filter_eq_generate

added theorem FilterBasis.eq_infᵢ_principal

added theorem FilterBasis.mem_filter_iff

added theorem FilterBasis.mem_filter_of_mem

added theorem FilterBasis.mem_sets

added structure FilterBasis

added theorem Pairwise.exists_mem_filter_basis_of_disjoint

added theorem Set.PairwiseDisjoint.exists_mem_filter_basis

Modified Mathlib/Order/Filter/Basic.lean