Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-12 14:09 f5a85f10

View on Github →

refactor(order/filter): move lift and lift' to separate file

Estimated changes

added theorem set.prod_eq_empty_iff
added theorem filter.bot_prod
deleted theorem filter.comap_eq_lift'
deleted theorem filter.comap_lift'_eq2
deleted theorem filter.comap_lift'_eq
deleted theorem filter.comap_lift_eq2
deleted theorem filter.comap_lift_eq
deleted theorem filter.le_lift'
deleted theorem filter.le_lift
deleted theorem filter.lift'_cong
deleted theorem filter.lift'_id
deleted theorem filter.lift'_infi
deleted theorem filter.lift'_le
deleted theorem filter.lift'_lift'_assoc
deleted theorem filter.lift'_lift_assoc
deleted theorem filter.lift'_mono'
deleted theorem filter.lift'_mono
deleted theorem filter.lift'_neq_bot_iff
deleted theorem filter.lift'_principal
deleted theorem filter.lift_assoc
deleted theorem filter.lift_comm
deleted theorem filter.lift_const
deleted theorem filter.lift_inf
deleted theorem filter.lift_infi'
deleted theorem filter.lift_infi
deleted theorem filter.lift_le
deleted theorem filter.lift_lift'_assoc
deleted theorem filter.lift_mono'
deleted theorem filter.lift_mono
deleted theorem filter.lift_neq_bot_iff
deleted theorem filter.lift_principal2
deleted theorem filter.lift_principal
deleted theorem filter.lift_sets_eq
deleted theorem filter.map_lift'_eq2
deleted theorem filter.map_lift'_eq
deleted theorem filter.map_lift_eq2
deleted theorem filter.map_lift_eq
deleted theorem filter.mem_lift'
deleted theorem filter.mem_lift'_sets
deleted theorem filter.mem_lift
deleted theorem filter.mem_lift_sets
deleted theorem filter.mem_prod_same_iff
deleted theorem filter.monotone_lift'
deleted theorem filter.monotone_lift
deleted theorem filter.principal_le_lift'
deleted theorem filter.prod_bot1
deleted theorem filter.prod_bot2
added theorem filter.prod_bot
deleted theorem filter.prod_def
added theorem filter.prod_eq_bot
deleted theorem filter.prod_lift'_lift'
deleted theorem filter.prod_lift_lift
deleted theorem filter.prod_same_eq
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.le_lift'
added theorem filter.le_lift
added theorem filter.lift'_cong
added theorem filter.lift'_id
added theorem filter.lift'_infi
added theorem filter.lift'_le
added theorem filter.lift'_mono'
added theorem filter.lift'_mono
added theorem filter.lift'_principal
added theorem filter.lift_assoc
added theorem filter.lift_comm
added theorem filter.lift_const
added theorem filter.lift_inf
added theorem filter.lift_infi'
added theorem filter.lift_infi
added theorem filter.lift_le
added theorem filter.lift_mono'
added theorem filter.lift_mono
added theorem filter.lift_principal2
added theorem filter.lift_principal
added theorem filter.lift_sets_eq
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.prod_def
added theorem filter.prod_lift_lift
added theorem filter.prod_same_eq