Skip to content

Commit

Permalink
fix(topology/continuous_on): avoid duplicate instance arguments (#1542)
Browse files Browse the repository at this point in the history
This was broken by #1516, caught by sanity_check.
  • Loading branch information
rwbarton authored and mergify[bot] committed Oct 12, 2019
1 parent 995add3 commit 92a9a78
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/topology/continuous_on.lean
Expand Up @@ -23,7 +23,7 @@ equipped with the subspace topology.
open set filter

variables {α : Type*} {β : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]
variables [topological_space α]

/-- The "neighborhood within" filter. Elements of `nhds_within a s` are sets containing the
intersection of `s` and a neighborhood of `a`. -/
Expand Down Expand Up @@ -181,6 +181,8 @@ theorem tendsto_nhds_within_iff_subtype {s : set α} {a : α} (h : a ∈ s) (f :
by rw [tendsto, tendsto, function.restrict, nhds_within_eq_map_subtype_val h,
←(@filter.map_map _ _ _ _ subtype.val)]

variables [topological_space β] [topological_space γ]

/-- A function between topological spaces is continuous at a point `x₀` within a subset `s`
if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. -/
def continuous_within_at (f : α → β) (s : set α) (x : α) : Prop :=
Expand Down

0 comments on commit 92a9a78

Please sign in to comment.