Skip to content

Commit

Permalink
remove empty line
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Nov 20, 2024
1 parent df893d8 commit b5236a3
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1135,7 +1135,6 @@ theorem dense_iff_iUnion_ball (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s,
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
forall_comm (α := α)]


theorem denseRange_iff {f : β → α} : DenseRange f ↔ ∀ x, ∀ r > 0, ∃ y, dist x (f y) < r :=
forall_congr' fun x => by simp only [mem_closure_iff, exists_range_iff]

Expand Down

0 comments on commit b5236a3

Please sign in to comment.