Skip to content

Commit

Permalink
fix: add space in unionₛ notation (#1209)
Browse files Browse the repository at this point in the history
  • Loading branch information
rwbarton committed Dec 24, 2022
1 parent 863ab3e commit c286e19
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Set/Lattice.lean
Expand Up @@ -87,7 +87,7 @@ def unionₛ (S : Set (Set α)) : Set α :=
#align set.sUnion Set.unionₛ

/-- Notation for Set.unionₛ`. Union of a set of sets. -/
prefix:110 "⋃₀" => unionₛ
prefix:110 "⋃₀ " => unionₛ

@[simp]
theorem mem_interₛ {x : α} {S : Set (Set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t :=
Expand Down

0 comments on commit c286e19

Please sign in to comment.