Skip to content

Commit

Permalink
Update UrysohnsLemma.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
yoh-tanimoto authored Apr 19, 2024
1 parent 9763e4c commit a0af4a0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Topology/UrysohnsLemma.lean
Original file line number Diff line number Diff line change
Expand Up @@ -642,7 +642,7 @@ lemma exists_forall_tsupport_iUnion_one_iUnion_of_isOpen_isClosed [NormalSpace X
all_goals
simp only [Finset.mem_filter, Finset.mem_univ, true_and, not_le]
rw [Fin.lt_def]
simp only [Fin.val_nat_cast]
simp only [Fin.val_natCast]
exact lt_add_one m
intro x hx
have huniv : {j : Fin (Nat.succ n) | j ≤ ⟨n, (lt_add_one n)⟩ }.toFinset = Finset.univ := by
Expand Down

0 comments on commit a0af4a0

Please sign in to comment.