Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-29 20:38 ebeeee7f

View on Github →

feat(filters): a couple more lemmas (#3625) Random lemmas gathered while thinking about https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nhds_left.20and.20nhds_right

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.union_distrib_Inter_left

added theorem set.union_distrib_Inter_right

Modified src/order/filter/bases.lean

added theorem filter.has_basis.ext

added theorem filter.has_basis.sup

added theorem filter.has_basis_binfi_principal'

Modified src/order/filter/basic.lean

added theorem filter.binfi_sup_left

added theorem filter.binfi_sup_right

deleted theorem filter.infi_sup_eq

added theorem filter.infi_sup_left

added theorem filter.infi_sup_right