Skip to content

Commit

Permalink
Undo an accidental change of namespace
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Feb 1, 2020
1 parent 992f858 commit b38a8fe
Showing 1 changed file with 3 additions and 7 deletions.
10 changes: 3 additions & 7 deletions src/data/set/function.lean
Original file line number Diff line number Diff line change
Expand Up @@ -23,19 +23,15 @@ universes u v w x y

variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}

namespace function
open function

namespace set

/-! ### Restrict -/

lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
by { ext x, simp [restrict], refl }

end function

open function

namespace set

variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} {p : set γ} {f f₁ f₂ f₃ : α → β} {g : β → γ}
{f' f₁' f₂' : β → α} {g' : γ → β}

Expand Down

0 comments on commit b38a8fe

Please sign in to comment.