Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-14 12:28 0e5f44b0

View on Github →

chore(*): assorted lemmas for FTC-1 (#3755) Lemmas from FTC-1 (has_strict_deriv version) #3709

Estimated changes

added theorem set.forall_prod_set
modified theorem set.mem_powerset_iff
added theorem set.monotone_powerset
added theorem set.powerset_empty
added theorem set.powerset_inter
modified theorem set.powerset_mono
modified theorem set.powerset_nonempty
modified theorem set.Ico_disjoint_Ico
modified theorem set.Ico_disjoint_Ico_same
added theorem set.Iic_disjoint_Ioc
added theorem set.Iic_disjoint_Ioi
modified theorem set.Ioc_disjoint_Ioc
modified theorem set.Ioc_disjoint_Ioc_same
added theorem filter.comap_pure
added theorem filter.eventually_pure
deleted theorem filter.pure_eq_principal
added theorem filter.pure_le_iff
modified theorem filter.tendsto_infi
modified theorem filter.tendsto_principal
modified theorem filter.tendsto_pure
added theorem filter.lift'_bot
added theorem filter.lift'_inf
added theorem filter.lift'_pure
added theorem pure_le_nhds_within