Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-30 22:10 f57e59f4

View on Github →

feat(data/analysis): calculations with filters / topologies + misc

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.exists_ne_one_of_prod_ne_one

modified theorem finset.prod_bind

added theorem finset.prod_eq_fold

modified theorem finset.prod_image

modified theorem finset.prod_insert

modified theorem finset.prod_sdiff

modified theorem finset.prod_sigma

modified theorem finset.prod_singleton

modified theorem finset.prod_union

modified theorem finset.prod_union_inter

Modified algebra/ordered_group.lean

modified theorem zero_le

Modified analysis/measure_theory/borel_space.lean

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

added theorem is_open_iff_mem_nhds

added theorem mem_interior_iff_mem_nhds

modified theorem topological_space.mem_nhds_of_is_topological_basis

Created data/analysis/filter.lean

added theorem cfilter.coe_mk

added theorem cfilter.mem_to_filter_sets

added def cfilter.of_equiv

added theorem cfilter.of_equiv_val

added def cfilter.to_filter

added structure cfilter

added theorem filter.realizer.bot_F

added theorem filter.realizer.bot_σ

added theorem filter.realizer.le_iff

added theorem filter.realizer.map_F

added theorem filter.realizer.map_σ

added theorem filter.realizer.mem_sets

added theorem filter.realizer.ne_bot_iff

added def filter.realizer.of_eq

added def filter.realizer.of_equiv

added theorem filter.realizer.of_equiv_F

added theorem filter.realizer.of_equiv_σ

added def filter.realizer.of_filter

added theorem filter.realizer.principal_F

added theorem filter.realizer.principal_σ

added theorem filter.realizer.tendsto_iff

added theorem filter.realizer.top_F

added theorem filter.realizer.top_σ

added structure filter.realizer

Created data/analysis/topology.lean

added def compact.realizer

added theorem ctop.coe_mk

added theorem ctop.mem_nhds_to_topsp

added def ctop.of_equiv

added theorem ctop.of_equiv_val

added theorem ctop.realizer.ext'

added theorem ctop.realizer.ext

added theorem ctop.realizer.is_closed_iff

added theorem ctop.realizer.is_open_iff

added theorem ctop.realizer.mem_interior_iff

added theorem ctop.realizer.nhds_F

added theorem ctop.realizer.nhds_σ

added def ctop.realizer.of_equiv

added theorem ctop.realizer.of_equiv_F

added theorem ctop.realizer.of_equiv_σ

added theorem ctop.realizer.tendsto_nhds_iff

added structure ctop.realizer

added theorem ctop.to_topsp_is_topological_basis

added structure ctop

added theorem locally_finite.realizer.to_locally_finite

added structure locally_finite.realizer

added theorem locally_finite_iff_exists_realizer

Modified data/equiv.lean

modified theorem equiv.apply_eq_iff_eq

modified theorem equiv.apply_inverse_apply

modified theorem equiv.inverse_apply_apply

Modified data/finset.lean

modified theorem finset.fold_image

modified theorem finset.fold_insert

modified theorem finset.fold_insert_idem

modified theorem finset.fold_singleton

modified theorem finset.fold_union_inter

modified theorem finset.image_singleton

added theorem finset.insert_empty_eq_singleton

deleted theorem finset.insert_singelton_self_eq

added theorem finset.insert_singleton_self_eq

added theorem finset.inter_eq_empty_iff_disjoint

modified theorem finset.inter_singleton_of_mem

modified theorem finset.inter_singleton_of_not_mem

modified theorem finset.mem_singleton

modified theorem finset.mem_singleton_self

added def finset.singleton

added theorem finset.singleton_eq_singleton

modified theorem finset.singleton_inj

modified theorem finset.singleton_inter_of_mem

modified theorem finset.singleton_inter_of_not_mem

modified theorem finset.singleton_ne_empty

modified theorem finset.singleton_val

Modified data/fintype.lean

added def fintype.card

added def fintype.equiv_fin

added theorem fintype.exists_equiv_fin

Modified data/list/basic.lean

added theorem list.nodup_iff_nth_le_inj

added theorem list.pairwise_iff_nth_le

Modified data/multiset.lean

Modified data/nat/prime.lean

added def nat.factors

Modified data/quot.lean

added theorem nonempty_of_trunc

Modified data/set/basic.lean

added theorem set.eq_univ_iff_forall

modified theorem set.eq_univ_of_forall

modified theorem set.inter_subset_left

modified theorem set.inter_subset_right

modified theorem set.range_id

added theorem set.range_iff_surjective

deleted theorem set.range_of_surjective

modified theorem set.subset_empty_iff

added theorem set.subset_eq_empty

added theorem set.subset_inter_iff

added theorem set.subset_ne_empty

Modified data/set/finite.lean

deleted inductive set.finite'

added theorem set.finite_mem_finset

Modified logic/basic.lean

added theorem iff_iff_eq

added theorem iff_of_eq

Modified order/basic.lean

modified def monotone

Modified order/filter.lean

added def filter.bind

modified theorem filter.bind_def

modified theorem filter.bind_mono2

modified theorem filter.bind_mono

modified theorem filter.bind_sup

deleted theorem filter.fmap_principal

added theorem filter.map_def

modified theorem filter.mem_bind_sets

modified theorem filter.principal_bind