Commit 2023-01-24 09:31 ea952b15

View on Github →

feat: port Order.Filter.Pi (#1802)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Pi.lean

added theorem Filter.NeBot.coprodᵢ

added theorem Filter.Tendsto.pi_map_coprodᵢ

added theorem Filter.compl_mem_coprodᵢ

added theorem Filter.coprodᵢ_bot'

added theorem Filter.coprodᵢ_bot

added theorem Filter.coprodᵢ_eq_bot_iff'

added theorem Filter.coprodᵢ_eq_bot_iff

added theorem Filter.coprodᵢ_mono

added theorem Filter.coprodᵢ_neBot

added theorem Filter.coprodᵢ_neBot_iff'

added theorem Filter.coprodᵢ_neBot_iff

added theorem Filter.hasBasis_pi

added theorem Filter.le_pi

added theorem Filter.map_eval_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 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_neBot

added theorem Filter.pi_inf_principal_univ_pi_eq_bot

added theorem Filter.pi_inf_principal_univ_pi_neBot

added theorem Filter.pi_inj

added theorem Filter.pi_le_pi

added theorem Filter.pi_mem_pi

added theorem Filter.pi_mem_pi_iff

added theorem Filter.pi_mono

added theorem Filter.pi_neBot

added theorem Filter.tendsto_eval_pi

added theorem Filter.tendsto_pi