feat(topology/continuous_function/{basic, compact}): add a few missin…

…g lemmas (#16714)

src/topology/continuous_function/basic.lean

@@ -80,6 +80,9 @@ instance : has_coe_to_fun (C(α, β)) (λ _, α → β) := fun_like.has_coe_to_f
 -- this must come after the coe_to_fun definition
 initialize_simps_projections continuous_map (to_fun → apply)
 
+@[protected, simp, norm_cast]
+lemma coe_coe {F : Type*} [continuous_map_class F α β] (f : F) : ⇑(f : C(α, β)) = f := rfl
+
 @[ext] lemma ext {f g : C(α, β)} (h : ∀ a, f a = g a) : f = g := fun_like.ext _ _ h
 
 /-- Copy of a `continuous_map` with a new `to_fun` equal to the old one. Useful to fix definitional

src/topology/continuous_function/compact.lean

@@ -185,10 +185,17 @@ lemma norm_le_of_nonempty [nonempty α] {M : ℝ} : ∥f∥ ≤ M ↔ ∀ x, ∥
 lemma norm_lt_iff {M : ℝ} (M0 : 0 < M) : ∥f∥ < M ↔ ∀ x, ∥f x∥ < M :=
 @bounded_continuous_function.norm_lt_iff_of_compact _ _ _ _ _ (mk_of_compact f) _ M0
 
+theorem nnnorm_lt_iff {M : ℝ≥0} (M0 : 0 < M) : ∥f∥₊ < M ↔ ∀ (x : α), ∥f x∥₊ < M :=
+f.norm_lt_iff M0
+
 lemma norm_lt_iff_of_nonempty [nonempty α] {M : ℝ} :
   ∥f∥ < M ↔ ∀ x, ∥f x∥ < M :=
 @bounded_continuous_function.norm_lt_iff_of_nonempty_compact _ _ _ _ _ _ (mk_of_compact f) _
 
+lemma nnnorm_lt_iff_of_nonempty [nonempty α] {M : ℝ≥0} :
+  ∥f∥₊ < M ↔ ∀ x, ∥f x∥₊ < M :=
+f.norm_lt_iff_of_nonempty
+
 lemma apply_le_norm (f : C(α, ℝ)) (x : α) : f x ≤ ∥f∥ :=
 le_trans (le_abs.mpr (or.inl (le_refl (f x)))) (f.norm_coe_le_norm x)