Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 07:38 6a48b384

View on Github →

feat(topology/uniform_space): lemmas about s ○ s ○ ... ○ s ⊆ t (#14051)

Estimated changes

Modified src/order/filter/small_sets.lean

added theorem filter.eventually_small_sets_subset

Modified src/topology/uniform_space/basic.lean

added theorem eventually_uniformity_comp_subset

added theorem eventually_uniformity_iterate_comp_subset

added theorem left_subset_comp_rel

added theorem right_subset_comp_rel

modified theorem subset_comp_self

added theorem subset_iterate_comp_rel

added theorem symmetric_rel.mk_mem_comm