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 `iff`s;
* drop `continuous_induced_rng'`;
* add `is_open_sup`.

src/geometry/manifold/instances/sphere.lean

@@ -167,7 +167,7 @@ begin
 end
 
 lemma continuous_stereo_inv_fun (hv : ∥v∥ = 1) : continuous (stereo_inv_fun hv) :=
-continuous_induced_rng (cont_diff_stereo_inv_fun_aux.continuous.comp continuous_subtype_coe)
+continuous_induced_rng.2 (cont_diff_stereo_inv_fun_aux.continuous.comp continuous_subtype_coe)
 
 variables [complete_space E]
 
@@ -386,7 +386,7 @@ lemma cont_mdiff.cod_restrict_sphere {n : ℕ} [fact (finrank ℝ E = n + 1)]
   cont_mdiff I (𝓡 n) m (set.cod_restrict _ _ hf' : M → (sphere (0:E) 1)) :=
 begin
   rw cont_mdiff_iff_target,
-  refine ⟨continuous_induced_rng hf.continuous, _⟩,
+  refine ⟨continuous_induced_rng.2 hf.continuous, _⟩,
   intros v,
   let U := -- Again, removing type ascription... Weird that this helps!
     (orthonormal_basis.from_orthogonal_span_singleton n (ne_zero_of_mem_unit_sphere (-v))).repr,

src/topology/algebra/constructions.lean

@@ -34,7 +34,7 @@ variables [topological_space M]
 continuous_induced_dom
 
 @[continuity, to_additive] lemma continuous_op : continuous (op : M → Mᵐᵒᵖ) :=
-continuous_induced_rng continuous_id
+continuous_induced_rng.2 continuous_id
 
 @[to_additive] instance [t2_space M] : t2_space Mᵐᵒᵖ :=
 ⟨λ x y h, separated_by_continuous mul_opposite.continuous_unop $ unop_injective.ne h⟩

src/topology/algebra/group.lean

@@ -279,7 +279,7 @@ variables {ι' : Sort*} [has_inv G]
 @[to_additive] lemma has_continuous_inv_Inf {ts : set (topological_space G)}
   (h : Π t ∈ ts, @has_continuous_inv G t _) :
   @has_continuous_inv G (Inf ts) _ :=
-{ continuous_inv := continuous_Inf_rng (λ t ht, continuous_Inf_dom ht
+{ continuous_inv := continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom ht
   (@has_continuous_inv.continuous_inv G t _ (h t ht))) }
 
 @[to_additive] lemma has_continuous_inv_infi {ts' : ι' → topological_space G}
@@ -1145,7 +1145,7 @@ variables [group G] [topological_space G] [topological_group G] {Γ : subgroup G
 @[to_additive]
 instance quotient_group.has_continuous_const_smul : has_continuous_const_smul G (G ⧸ Γ) :=
 { continuous_const_smul := λ g₀, begin
-    apply continuous_coinduced_dom,
+    apply continuous_coinduced_dom.2,
     change continuous (λ g : G, quotient_group.mk (g₀ * g)),
     exact continuous_coinduced_rng.comp (continuous_mul_left g₀),
   end }
@@ -1181,7 +1181,7 @@ variables [monoid α] [topological_space α] [has_continuous_mul α] [monoid β]
   [has_continuous_mul β]
 
 @[to_additive] instance : topological_group αˣ :=
-{ continuous_inv := continuous_induced_rng ((continuous_unop.comp
+{ continuous_inv := continuous_induced_rng.2 ((continuous_unop.comp
     (@continuous_embed_product α _ _).snd).prod_mk (continuous_op.comp continuous_coe)) }
 
 /-- The topological group isomorphism between the units of a product of two monoids, and the product
@@ -1191,21 +1191,21 @@ def homeomorph.prod_units : homeomorph (α × β)ˣ (αˣ × βˣ) :=
   begin
     show continuous (λ i : (α × β)ˣ, (map (monoid_hom.fst α β) i, map (monoid_hom.snd α β) i)),
     refine continuous.prod_mk _ _,
-    { refine continuous_induced_rng ((continuous_fst.comp units.continuous_coe).prod_mk _),
+    { refine continuous_induced_rng.2 ((continuous_fst.comp units.continuous_coe).prod_mk _),
       refine mul_opposite.continuous_op.comp (continuous_fst.comp _),
       simp_rw units.inv_eq_coe_inv,
       exact units.continuous_coe.comp continuous_inv, },
-    { refine continuous_induced_rng ((continuous_snd.comp units.continuous_coe).prod_mk _),
+    { refine continuous_induced_rng.2 ((continuous_snd.comp units.continuous_coe).prod_mk _),
       simp_rw units.coe_map_inv,
       exact continuous_op.comp (continuous_snd.comp (units.continuous_coe.comp continuous_inv)), }
   end,
   continuous_inv_fun :=
   begin
-    refine continuous_induced_rng (continuous.prod_mk _ _),
+    refine continuous_induced_rng.2 (continuous.prod_mk _ _),
     { exact (units.continuous_coe.comp continuous_fst).prod_mk
         (units.continuous_coe.comp continuous_snd), },
     { refine continuous_op.comp
-        (units.continuous_coe.comp $ continuous_induced_rng $ continuous.prod_mk _ _),
+        (units.continuous_coe.comp $ continuous_induced_rng.2 $ continuous.prod_mk _ _),
       { exact (units.continuous_coe.comp (continuous_inv.comp continuous_fst)).prod_mk
           (units.continuous_coe.comp (continuous_inv.comp continuous_snd)) },
       { exact continuous_op.comp ((units.continuous_coe.comp continuous_fst).prod_mk

src/topology/algebra/module/basic.lean

@@ -139,7 +139,7 @@ lemma has_continuous_smul_induced :
 { continuous_smul :=
     begin
       letI : topological_space M₁ := t.induced f,
-      refine continuous_induced_rng _,
+      refine continuous_induced_rng.2 _,
       simp_rw [function.comp, f.map_smul],
       refine continuous_fst.smul (continuous_induced_dom.comp continuous_snd)
     end }

src/topology/algebra/module/weak_dual.lean

@@ -104,7 +104,7 @@ lemma eval_continuous (y : F) : continuous (λ x : weak_bilin B, B x y) :=
 
 lemma continuous_of_continuous_eval [topological_space α] {g : α → weak_bilin B}
   (h : ∀ y, continuous (λ a, B (g a) y)) : continuous g :=
-continuous_induced_rng (continuous_pi_iff.mpr h)
+continuous_induced_rng.2 (continuous_pi_iff.mpr h)
 
 /-- The coercion `(λ x y, B x y) : E → (F → 𝕜)` is an embedding. -/
 lemma embedding {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : function.injective B) :
@@ -118,7 +118,7 @@ by rw [← tendsto_pi_nhds, embedding.tendsto_nhds_iff (embedding hB)]
 /-- Addition in `weak_space B` is continuous. -/
 instance [has_continuous_add 𝕜] : has_continuous_add (weak_bilin B) :=
 begin
-  refine ⟨continuous_induced_rng _⟩,
+  refine ⟨continuous_induced_rng.2 _⟩,
   refine cast (congr_arg _ _) (((coe_fn_continuous B).comp continuous_fst).add
     ((coe_fn_continuous B).comp continuous_snd)),
   ext,
@@ -128,7 +128,7 @@ end
 /-- Scalar multiplication by `𝕜` on `weak_bilin B` is continuous. -/
 instance [has_continuous_smul 𝕜 𝕜] : has_continuous_smul 𝕜 (weak_bilin B) :=
 begin
-  refine ⟨continuous_induced_rng _⟩,
+  refine ⟨continuous_induced_rng.2 _⟩,
   refine cast (congr_arg _ _) (continuous_fst.smul ((coe_fn_continuous B).comp continuous_snd)),
   ext,
   simp only [function.comp_app, pi.smul_apply, linear_map.map_smulₛₗ, ring_hom.id_apply,
@@ -149,7 +149,7 @@ continuous. -/
 instance [has_continuous_add 𝕜] : topological_add_group (weak_bilin B) :=
 { to_has_continuous_add := by apply_instance,
   continuous_neg := begin
-    refine continuous_induced_rng (continuous_pi_iff.mpr (λ y, _)),
+    refine continuous_induced_rng.2 (continuous_pi_iff.mpr (λ y, _)),
     refine cast (congr_arg _ _) (eval_continuous B (-y)),
     ext,
     simp only [map_neg, function.comp_app, linear_map.neg_apply],
@@ -217,14 +217,14 @@ continuous_linear_map.module
 
 instance (M) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜]
   [has_continuous_const_smul M 𝕜] : has_continuous_const_smul M (weak_dual 𝕜 E) :=
-⟨λ m, continuous_induced_rng $ (weak_bilin.coe_fn_continuous (top_dual_pairing 𝕜 E)).const_smul m⟩
+⟨λ m, continuous_induced_rng.2 $ (weak_bilin.coe_fn_continuous (top_dual_pairing 𝕜 E)).const_smul m⟩
 
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it continuously acts on `weak_dual 𝕜 E`. -/
 instance (M) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜]
   [topological_space M] [has_continuous_smul M 𝕜] :
   has_continuous_smul M (weak_dual 𝕜 E) :=
-⟨continuous_induced_rng $ continuous_fst.smul ((weak_bilin.coe_fn_continuous
+⟨continuous_induced_rng.2 $ continuous_fst.smul ((weak_bilin.coe_fn_continuous
                           (top_dual_pairing 𝕜 E)).comp continuous_snd)⟩
 
 lemma coe_fn_continuous : continuous (λ (x : weak_dual 𝕜 E) y, x y) :=
@@ -235,7 +235,7 @@ continuous_pi_iff.mp coe_fn_continuous y
 
 lemma continuous_of_continuous_eval [topological_space α] {g : α → weak_dual 𝕜 E}
   (h : ∀ y, continuous (λ a, (g a) y)) : continuous g :=
-continuous_induced_rng (continuous_pi_iff.mpr h)
+continuous_induced_rng.2 (continuous_pi_iff.mpr h)
 
 end weak_dual
 

src/topology/algebra/monoid.lean

@@ -565,7 +565,7 @@ variables {ι' : Sort*} [has_mul M]
 @[to_additive] lemma has_continuous_mul_Inf {ts : set (topological_space M)}
   (h : Π t ∈ ts, @has_continuous_mul M t _) :
   @has_continuous_mul M (Inf ts) _ :=
-{ continuous_mul := continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ ht ht
+{ continuous_mul := continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom₂ ht ht
   (@has_continuous_mul.continuous_mul M t _ (h t ht))) }
 
 @[to_additive] lemma has_continuous_mul_infi {ts : ι' → topological_space M}

src/topology/algebra/mul_action.lean

@@ -154,7 +154,7 @@ variables {ι : Sort*} {M X : Type*} [topological_space M] [has_smul M X]
 { continuous_smul :=
   begin
     rw ← @Inf_singleton _ _ ‹topological_space M›,
-    exact continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
+    exact continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
       (@has_continuous_smul.continuous_smul _ _ _ _ t (h t ht)))
   end }
 

src/topology/algebra/ring.lean

@@ -160,15 +160,15 @@ open mul_opposite
 
 instance [non_unital_non_assoc_semiring α] [topological_space α] [has_continuous_add α] :
   has_continuous_add αᵐᵒᵖ :=
-{ continuous_add := continuous_induced_rng $ (@continuous_add α _ _ _).comp
+{ continuous_add := continuous_induced_rng.2 $ (@continuous_add α _ _ _).comp
   (continuous_unop.prod_map continuous_unop) }
 
 instance [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] :
   topological_semiring αᵐᵒᵖ := {}
 
 instance [non_unital_non_assoc_ring α] [topological_space α] [has_continuous_neg α] :
   has_continuous_neg αᵐᵒᵖ :=
-{ continuous_neg := continuous_induced_rng $ (@continuous_neg α _ _ _).comp continuous_unop }
+{ continuous_neg := continuous_induced_rng.2 $ (@continuous_neg α _ _ _).comp continuous_unop }
 
 instance [non_unital_non_assoc_ring α] [topological_space α] [topological_ring α] :
   topological_ring αᵐᵒᵖ := {}
@@ -379,23 +379,23 @@ let Inf_S' := Inf (to_topological_space '' S) in
 { to_topological_space := Inf_S',
   continuous_add       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     have h_continuous_id := @continuous.prod_map _ _ _ _ t t Inf_S' Inf_S' _ _ h h,
     exact @continuous.comp _ _ _ (id _) (id _) t _ _ continuous_add h_continuous_id,
   end,
   continuous_mul       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     have h_continuous_id := @continuous.prod_map _ _ _ _ t t Inf_S' Inf_S' _ _ h h,
     exact @continuous.comp _ _ _ (id _) (id _) t _ _ continuous_mul h_continuous_id,
   end,
   continuous_neg       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     exact @continuous.comp _ _ _ (id _) (id _) t _ _ continuous_neg h,

src/topology/algebra/star.lean

@@ -84,6 +84,6 @@ instance [has_star R] [topological_space R] [has_continuous_star R] : has_contin
 
 instance [monoid R] [star_semigroup R] [topological_space R] [has_continuous_star R] :
   has_continuous_star Rˣ :=
-⟨continuous_induced_rng units.continuous_embed_product.star⟩
+⟨continuous_induced_rng.2 units.continuous_embed_product.star⟩
 
 end instances

src/topology/constructions.lean

@@ -230,7 +230,7 @@ hf.comp continuous_at_snd
 
 @[continuity] lemma continuous.prod_mk {f : γ → α} {g : γ → β}
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
-continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
+continuous_inf_rng.2 ⟨continuous_induced_rng.2 hf, continuous_induced_rng.2 hg⟩
 
 @[continuity] lemma continuous.prod.mk (a : α) : continuous (λ b : β, (a, b)) :=
 continuous_const.prod_mk continuous_id'
@@ -626,11 +626,8 @@ continuous_sup_rng_right continuous_coinduced_rng
 
 @[continuity] lemma continuous.sum_elim {f : α → γ} {g : β → γ}
   (hf : continuous f) (hg : continuous g) : continuous (sum.elim f g) :=
-begin
-  apply continuous_sup_dom;
-  rw continuous_def at hf hg ⊢;
-  assumption
-end
+by simp only [continuous_sup_dom, continuous_coinduced_dom, sum.elim_comp_inl, sum.elim_comp_inr,
+  true_and, *]
 
 @[continuity] lemma continuous.sum_map {f : α → β} {g : γ → δ}
   (hf : continuous f) (hg : continuous g) : continuous (sum.map f g) :=
@@ -760,7 +757,7 @@ lemma is_closed.closed_embedding_subtype_coe {s : set α} (hs : is_closed s) :
 
 @[continuity] lemma continuous_subtype_mk {f : β → α}
   (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
-continuous_induced_rng h
+continuous_induced_rng.2 h
 
 lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) :=
 continuous_subtype_mk _ continuous_subtype_coe
@@ -850,7 +847,7 @@ continuous_coinduced_rng
 
 @[continuity] lemma continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b)
   (h : continuous f) : continuous (quot.lift f hr : quot r → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 lemma quotient_map_quotient_mk : quotient_map (@quotient.mk α s) :=
 quotient_map_quot_mk
@@ -860,11 +857,11 @@ continuous_coinduced_rng
 
 lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
   (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 lemma continuous_quotient_lift_on' {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
   (h : continuous f) : continuous (λ x, quotient.lift_on' x f hs : quotient s → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 end quotient
 
@@ -874,7 +871,7 @@ variables {ι : Type*} {π : ι → Type*}
 @[continuity]
 lemma continuous_pi [topological_space α] [∀i, topological_space (π i)] {f : α → Πi:ι, π i}
   (h : ∀i, continuous (λa, f a i)) : continuous f :=
-continuous_infi_rng $ assume i, continuous_induced_rng $ h i
+continuous_infi_rng.2 $ assume i, continuous_induced_rng.2 $ h i
 
 @[continuity]
 lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
@@ -1135,7 +1132,7 @@ end
 @[continuity]
 lemma continuous_sigma [topological_space β] {f : sigma σ → β}
   (h : ∀ i, continuous (λ a, f ⟨i, a⟩)) : continuous f :=
-continuous_supr_dom (λ i, continuous_coinduced_dom (h i))
+continuous_supr_dom.2 (λ i, continuous_coinduced_dom.2 (h i))
 
 @[continuity]
 lemma continuous_sigma_map {κ : Type*} {τ : κ → Type*} [Π k, topological_space (τ k)]
@@ -1201,7 +1198,7 @@ continuous_induced_dom
 
 @[continuity] lemma continuous_ulift_up [topological_space α] :
   continuous (ulift.up : α → ulift.{v u} α) :=
-continuous_induced_rng continuous_id
+continuous_induced_rng.2 continuous_id
 
 end ulift
 

src/topology/continuous_function/units.lean

@@ -35,7 +35,7 @@ def units_lift : C(X, Mˣ) ≃ C(X, M)ˣ :=
   inv_fun := λ f,
   { to_fun := λ x, ⟨f x, f⁻¹ x, continuous_map.congr_fun f.mul_inv x,
                                 continuous_map.congr_fun f.inv_mul x⟩,
-    continuous_to_fun := continuous_induced_rng $ continuous.prod_mk (f : C(X, M)).continuous
+    continuous_to_fun := continuous_induced_rng.2 $ continuous.prod_mk (f : C(X, M)).continuous
       $ mul_opposite.continuous_op.comp (↑f⁻¹ : C(X, M)).continuous },
   left_inv := λ f, by { ext, refl },
   right_inv := λ f, by { ext, refl } }
@@ -49,7 +49,7 @@ variables [normed_ring R] [complete_space R]
 lemma _root_.normed_ring.is_unit_unit_continuous {f : C(X, R)} (h : ∀ x, is_unit (f x)) :
   continuous (λ x, (h x).unit) :=
 begin
-  refine continuous_induced_rng (continuous.prod_mk f.continuous
+  refine continuous_induced_rng.2 (continuous.prod_mk f.continuous
     (mul_opposite.continuous_op.comp (continuous_iff_continuous_at.mpr (λ x, _)))),
   have := normed_ring.inverse_continuous_at (h x).unit,
   simp only [←ring.inverse_unit, is_unit.unit_spec, ←function.comp_apply] at this ⊢,