Commit 2023-01-24 09:37 9742cd11

View on Github →

feat: port Order.Filter.Lift (#1804)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Lift.lean

added theorem Filter.HasBasis.lift'

added theorem Filter.HasBasis.lift

added theorem Filter.HasBasis.mem_lift_iff

added theorem Filter.comap_eq_lift'

added theorem Filter.comap_lift'_eq2

added theorem Filter.comap_lift'_eq

added theorem Filter.comap_lift_eq2

added theorem Filter.comap_lift_eq

added theorem Filter.eventually_lift'_iff

added theorem Filter.interₛ_lift'_sets

added theorem Filter.interₛ_lift_sets

added theorem Filter.le_lift'

added theorem Filter.le_lift

added theorem Filter.lift'_bot

added theorem Filter.lift'_cong

added theorem Filter.lift'_id

added theorem Filter.lift'_inf

added theorem Filter.lift'_inf_le

added theorem Filter.lift'_inf_principal_eq

added theorem Filter.lift'_infᵢ

added theorem Filter.lift'_infᵢ_of_map_univ

added theorem Filter.lift'_le

added theorem Filter.lift'_lift'_assoc

added theorem Filter.lift'_lift_assoc

added theorem Filter.lift'_map_le

added theorem Filter.lift'_mono'

added theorem Filter.lift'_mono

added theorem Filter.lift'_neBot_iff

added theorem Filter.lift'_principal

added theorem Filter.lift'_pure

added theorem Filter.lift'_top

added theorem Filter.lift_assoc

added theorem Filter.lift_comm

added theorem Filter.lift_const

added theorem Filter.lift_inf

added theorem Filter.lift_infᵢ

added theorem Filter.lift_infᵢ_le

added theorem Filter.lift_infᵢ_of_directed

added theorem Filter.lift_infᵢ_of_map_univ

added theorem Filter.lift_le

added theorem Filter.lift_lift'_assoc

added theorem Filter.lift_lift'_same_eq_lift'

added theorem Filter.lift_lift'_same_le_lift'

added theorem Filter.lift_lift_same_eq_lift

added theorem Filter.lift_lift_same_le_lift

added theorem Filter.lift_map_le

added theorem Filter.lift_mono'

added theorem Filter.lift_mono

added theorem Filter.lift_neBot_iff

added theorem Filter.lift_principal2

added theorem Filter.lift_principal

added theorem Filter.lift_top

added theorem Filter.map_lift'_eq2

added theorem Filter.map_lift'_eq

added theorem Filter.map_lift_eq2

added theorem Filter.map_lift_eq

added theorem Filter.mem_lift'

added theorem Filter.mem_lift'_sets

added theorem Filter.mem_lift

added theorem Filter.mem_lift_sets

added theorem Filter.monotone_lift'

added theorem Filter.monotone_lift

added theorem Filter.principal_le_lift'

added theorem Filter.prod_def

added theorem Filter.prod_lift'_lift'

added theorem Filter.prod_lift_lift

added theorem Filter.prod_same_eq

added theorem Filter.tendsto_lift'

added theorem Filter.tendsto_lift

added theorem Filter.tendsto_prod_self_iff