Skip to content

Commit

Permalink
doc: fix typo introduced in #11869 (#11889)
Browse files Browse the repository at this point in the history
  • Loading branch information
ADedecker authored and atarnoam committed Apr 16, 2024
1 parent 3daf5dd commit 0647d48
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Topology/Separation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1389,7 +1389,7 @@ theorem tendsto_nhds_unique_of_frequently_eq [T2Space X] {f g : Y → X} {l : Fi
/-- If `s` and `t` are compact sets in a T₂ space, then the set neighborhoods filter of `s ∩ t`
is the infimum of set neighborhoods filters for `s` and `t`.
For general sets, only the `≤` inequality holds, see `nhdsSet_inf_le`. -/
For general sets, only the `≤` inequality holds, see `nhdsSet_inter_le`. -/
theorem IsCompact.nhdsSet_inter_eq [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t := by
refine le_antisymm (nhdsSet_inter_le _ _) ?_
Expand Down

0 comments on commit 0647d48

Please sign in to comment.