Commit 2020-08-14 15:47 c2528003

View on Github →

chore(*): use notation for filter.prod (#3768) Also change from ∀ v w ∈ V to ∀ (v ∈ V) (w ∈ V) in exists_nhds_split_inv, exists_nhds_half_neg, add_group_with_zero_nhd.exists_Z_half.

Estimated changes

Modified src/analysis/calculus/fderiv.lean

Modified src/order/filter/bases.lean

added theorem filter.mem_prod_self_iff

Modified src/order/filter/basic.lean

modified theorem filter.prod_eq

Modified src/order/filter/lift.lean

modified theorem filter.prod_def

modified theorem filter.prod_same_eq

Modified src/topology/algebra/group.lean

modified theorem add_group_with_zero_nhd.add_Z

modified theorem add_group_with_zero_nhd.exists_Z_half

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/constructions.lean

modified theorem nhds_prod_eq

Modified src/topology/continuous_on.lean

Modified src/topology/list.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean

modified def cauchy

Modified src/topology/uniform_space/completion.lean

Modified src/topology/uniform_space/uniform_embedding.lean