Mathlib Changelog
Changelog
About
Github
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