Commit 2020-09-27 16:34 2516d7d6

View on Github →

feat(topology): various additions (#4264) Some if it is used for Fubini, but some of the results were rabbit holes I went into, which I never ended up using, but that still seem useful.

Estimated changes

Modified src/order/liminf_limsup.lean

added theorem filter.has_basis.Liminf_eq_supr_Inf

added theorem filter.has_basis.liminf_eq_supr_infi

added theorem filter.has_basis.limsup_eq_infi_supr

modified theorem filter.liminf_eq_supr_infi_of_nat'

modified theorem filter.liminf_eq_supr_infi_of_nat

modified theorem filter.limsup_eq_infi_supr_of_nat'

modified theorem filter.limsup_eq_infi_supr_of_nat

Modified src/topology/algebra/infinite_sum.lean

added theorem pi.has_sum

added theorem pi.summable

added theorem tsum_apply

Modified src/topology/algebra/ordered.lean

added theorem is_closed_le_prod

added theorem is_open_lt_prod

Modified src/topology/constructions.lean

added theorem tendsto_pi

Modified src/topology/instances/ennreal.lean

Modified src/topology/list.lean

added theorem filter.tendsto.cons

added theorem list.continuous_cons

added theorem list.continuous_prod

deleted theorem list.tendsto_cons'

modified theorem list.tendsto_cons

modified theorem list.tendsto_insert_nth

added theorem list.tendsto_prod

modified theorem nhds_cons

modified theorem nhds_list

modified theorem nhds_nil

modified theorem vector.continuous_at_remove_nth

modified theorem vector.continuous_insert_nth'

modified theorem vector.continuous_insert_nth

modified theorem vector.continuous_remove_nth

modified theorem vector.tendsto_cons

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem metric.coe_inf_nndist

added theorem metric.continuous_inf_nndist_pt

added def metric.inf_nndist

added theorem metric.lipschitz_inf_nndist_pt

added theorem metric.uniform_continuous_inf_nndist_pt