Skip to content

Commit

Permalink
fix(topology/continuous_function/basic): fix continuous_map.id_coe (#…
Browse files Browse the repository at this point in the history
  • Loading branch information
shingtaklam1324 committed Jul 2, 2021
1 parent 9e9dfc2 commit f5a8b8a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/topology/continuous_function/basic.lean
Expand Up @@ -81,7 +81,7 @@ end
/-- The identity as a continuous map. -/
def id : C(α, α) := ⟨id⟩

@[simp] lemma id_coe : (id : α → α) = id := rfl
@[simp] lemma id_coe : (id : α → α) = _root_.id := rfl
lemma id_apply (a : α) : id a = a := rfl

/-- The composition of continuous maps, as a continuous map. -/
Expand Down

0 comments on commit f5a8b8a

Please sign in to comment.