Commit 2022-05-02 17:28 917b5275

View on Github →

feat(topology/metric_space/thickened_indicator): Add definition and lemmas about thickened indicators. (#13481) Add thickened indicators, to be used for the proof of the portmanteau theorem.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.div_le_div

Modified src/topology/instances/ennreal.lean

Created src/topology/metric_space/thickened_indicator.lean

added theorem continuous_thickened_indicator_aux

added theorem thickened_indicator.coe_fn_eq_comp

added def thickened_indicator

added def thickened_indicator_aux

added theorem thickened_indicator_aux_closure_eq

added theorem thickened_indicator_aux_le_one

added theorem thickened_indicator_aux_lt_top

added theorem thickened_indicator_aux_mono

added theorem thickened_indicator_aux_one

added theorem thickened_indicator_aux_one_of_mem_closure

added theorem thickened_indicator_aux_subset

added theorem thickened_indicator_aux_tendsto_indicator_closure

added theorem thickened_indicator_aux_zero

added theorem thickened_indicator_le_one

added theorem thickened_indicator_mono

added theorem thickened_indicator_one

added theorem thickened_indicator_one_of_mem_closure

added theorem thickened_indicator_subset

added theorem thickened_indicator_tendsto_indicator_closure

added theorem thickened_indicator_zero