Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 11:08 8ad82e4b

View on Github →

feat(topology/order): upgrade some lemmas to iffs (#15617)

  • turn continuous_induced_rng, continuous_coinduced_dom, continuous_sup_dom, continuous_Sup_dom, continuous_supr_dom, continuous_inf_rng, continuous_Inf_rng, and continuous_infi_rng into iffs;
  • drop continuous_induced_rng';
  • add is_open_sup.

Estimated changes

modified theorem continuous_Inf_rng
modified theorem continuous_Sup_dom
modified theorem continuous_coinduced_dom
deleted theorem continuous_induced_rng'
modified theorem continuous_induced_rng
modified theorem continuous_inf_rng
modified theorem continuous_infi_rng
modified theorem continuous_sup_dom
modified theorem continuous_supr_dom
added theorem is_open_sup