Skip to content

Commit 08becba

Browse files
committed
doc(Data/Setoid/Partition): fix typo in module docstring (leanprover-community#37672)
An `IndexedPartition` is a function `ι → Set α` whose image is a partition, not a function `ι → α`.
1 parent 49358d7 commit 08becba

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Data/Setoid/Partition.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ This file comprises properties of equivalence relations viewed as partitions.
1515
There are two implementations of partitions here:
1616
* A collection `c : Set (Set α)` of sets is a partition of `α` if `∅ ∉ c` and each element `a : α`
1717
belongs to a unique set `b ∈ c`. This is expressed as `IsPartition c`
18-
* An indexed partition is a map `s : ι → α` whose image is a partition. This is
18+
* An indexed partition is a map `s : ι → Set α` whose image is a partition. This is
1919
expressed as `IndexedPartition s`.
2020
2121
Of course both implementations are related to `Quotient` and `Setoid`.

0 commit comments

Comments
 (0)