Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-23 17:17 a54be050

View on Github →

feat(analysis/topology): add continuity rules for supr, Sup, and pi spaces

Estimated changes

Modified analysis/topology/continuity.lean

modified theorem compact_pi_infinite

modified theorem continuous_Inf_rng

added theorem continuous_Sup_dom

added theorem continuous_Sup_rng

added theorem continuous_apply

modified theorem continuous_infi_rng

added theorem continuous_pi

modified theorem continuous_subtype_nhds_cover

added theorem continuous_supr_dom

added theorem continuous_supr_rng

modified theorem nhds_pi