Theorem filter.tendsto_inf_left

feat(order/filter): reorder filter theory; add filter_upwards tactic

feat(data/real,*): supporting material for metric spaces

feat(topology/ennreal): ennreal forms a topological monoid