Skip to content

Commit

Permalink
doc: typo in properVAdd_iff_continuousVadd_ultrafilter_tendsto (#17008
Browse files Browse the repository at this point in the history
)

Just a typo in the doc.
  • Loading branch information
Etienne committed Sep 24, 2024
1 parent ac554e7 commit 18506a8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Topology/Algebra/ProperAction.lean
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ instance (priority := 100) ProperSMul.toContinuousSMul [ProperSMul G X] : Contin
/-- A group `G` acts properly on a topological space `X` if and only if for all ultrafilters
`𝒰` on `X × G`, if `𝒰` converges to `(x₁, x₂)` along the map `(g, x) ↦ (g • x, x)`,
then there exists `g : G` such that `g • x₂ = x₁` and `𝒰.fst` converges to `g`. -/
@[to_additive "A group acts `G` properly on a topological space `X` if and only if
@[to_additive "A group `G` acts properly on a topological space `X` if and only if
for all ultrafilters `𝒰` on `X`, if `𝒰` converges to `(x₁, x₂)`
along the map `(g, x) ↦ (g • x, x)`, then there exists `g : G` such that `g • x₂ = x₁`
and `𝒰.fst` converges to `g`."]
Expand Down

0 comments on commit 18506a8

Please sign in to comment.