Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 11:49 9cf6766f

View on Github →

feat(order/filter/pi): define filter.pi and prove some properties (#10323)

Estimated changes

Modified src/analysis/box_integral/box/subbox_induction.lean

Modified src/analysis/calculus/tangent_cone.lean

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/constructions/pi.lean

deleted theorem measure_theory.measure.ae_pi_le_infi_comap

added theorem measure_theory.measure.ae_pi_le_pi

Modified src/measure_theory/constructions/prod.lean

Modified src/measure_theory/function/strongly_measurable.lean

Modified src/measure_theory/measure/haar_lebesgue.lean

Modified src/order/filter/basic.lean

deleted theorem filter.Coprod_mono

deleted theorem filter.Coprod_ne_bot

deleted theorem filter.Coprod_ne_bot_iff'

deleted theorem filter.Coprod_ne_bot_iff

deleted theorem filter.compl_mem_Coprod_iff

deleted theorem filter.map_pi_map_Coprod_le

deleted theorem filter.mem_Coprod_iff

deleted theorem filter.ne_bot.Coprod

deleted theorem filter.tendsto.pi_map_Coprod

Modified src/order/filter/cofinite.lean

Created src/order/filter/pi.lean

added theorem filter.Coprod_mono

added theorem filter.Coprod_ne_bot

added theorem filter.Coprod_ne_bot_iff'

added theorem filter.Coprod_ne_bot_iff

added theorem filter.compl_mem_Coprod_iff

added theorem filter.le_pi

added theorem filter.map_pi_map_Coprod_le

added theorem filter.mem_Coprod_iff

added theorem filter.mem_of_pi_mem_pi

added theorem filter.mem_pi'

added theorem filter.mem_pi

added theorem filter.mem_pi_of_mem

added theorem filter.ne_bot.Coprod

added def filter.pi

added theorem filter.pi_eq_bot

added theorem filter.pi_inf_principal_pi_eq_bot

added theorem filter.pi_inf_principal_pi_ne_bot

added theorem filter.pi_inf_principal_univ_pi_eq_bot

added theorem filter.pi_inf_principal_univ_pi_ne_bot

added theorem filter.pi_mem_pi

added theorem filter.pi_mem_pi_iff

added theorem filter.pi_mono

added theorem filter.pi_ne_bot

added theorem filter.tendsto.pi_map_Coprod

added theorem filter.tendsto_eval_pi

added theorem filter.tendsto_pi

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/ordered/basic.lean

Modified src/topology/algebra/ordered/monotone_convergence.lean

Modified src/topology/algebra/weak_dual_topology.lean

Modified src/topology/bases.lean

Modified src/topology/constructions.lean

modified theorem interior_pi_set

added theorem mem_nhds_of_pi_mem_nhds

deleted theorem mem_nhds_pi

modified theorem set_pi_mem_nhds_iff

deleted theorem tendsto_pi

added theorem tendsto_pi_nhds

Modified src/topology/continuous_on.lean

deleted theorem nhds_within_pi_univ_eq_bot

Modified src/topology/sequences.lean

Modified src/topology/subset_properties.lean

Modified src/topology/uniform_space/pi.lean