Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-24 09:09 69099f00

View on Github →

feat(order/filter/bases): define filter.has_basis (#1896)

feat(*): assorted simple lemmas, simplify some proofs
feat(order/filter/bases): define filter.has_basis
Add @[nolint]
+1 lemma, +1 simplified proof
Remove whitespaces Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Ref. note nolint_ge

Estimated changes

Created src/order/filter/bases.lean

added theorem filter.at_top_basis'

added theorem filter.at_top_basis

added theorem filter.basis_sets

added theorem filter.has_basis.comap

added theorem filter.has_basis.eq_binfi

added theorem filter.has_basis.eq_infi

added theorem filter.has_basis.forall_nonempty_iff_ne_bot

added theorem filter.has_basis.ge_iff

added theorem filter.has_basis.inf

added theorem filter.has_basis.inf_principal

added theorem filter.has_basis.le_basis_iff

added theorem filter.has_basis.le_iff

added theorem filter.has_basis.map

added theorem filter.has_basis.mem_iff

added theorem filter.has_basis.mem_of_mem

added theorem filter.has_basis.mem_of_superset

added theorem filter.has_basis.prod

added theorem filter.has_basis.prod_self

added theorem filter.has_basis.tendsto_iff

added theorem filter.has_basis.tendsto_left_iff

added theorem filter.has_basis.tendsto_right_iff

added theorem filter.has_basis_binfi_principal

added theorem filter.has_basis_infi_principal

added theorem filter.tendsto.basis_both

added theorem filter.tendsto.basis_left

added theorem filter.tendsto.basis_right