Skip to content

Commit

Permalink
Reorder words in sets.md (#594)
Browse files Browse the repository at this point in the history
Just a tiny change for clarity, matches the order of the descriptions to
that of the functions.
  • Loading branch information
ericluap authored Feb 19, 2025
1 parent 72cd7d7 commit 47111a0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion templates/theories/sets.md
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ Using `Classical.choose`, you can produce an object of type `Fintype s` from a p

### Cardinals

There are three functions `Finset.card`, `Fintype.card` and `Multiset.card`, which refer to the sizes of finsets, multisets and finite types. For finite cardinals of sets, `Fintype.card` can be used, given a proof that the set is finite.
There are three functions `Finset.card`, `Fintype.card` and `Multiset.card`, which refer to the sizes of finsets, finite types and multisets. For finite cardinals of sets, `Fintype.card` can be used, given a proof that the set is finite.

```lean
example : ∀ n : ℕ, Fintype.card (Fin n) = n := Fintype.card_fin
Expand Down

0 comments on commit 47111a0

Please sign in to comment.