feat(topology/order): upgrade some lemmas to `iff`s (#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 `iff`s;
* drop `continuous_induced_rng'`;
* add `is_open_sup`.
