We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a0ead74 commit e7ef425Copy full SHA for e7ef425
1 file changed
Mathlib/Data/Finset/Pi.lean
@@ -44,7 +44,7 @@ variable {β : α → Type u} {δ : α → Sort v} {s : Finset α} {t : ∀ a, F
44
section
45
variable [DecidableEq α]
46
47
-/-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
+/-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `β a`, then one can define the
48
finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
49
Note that the elements of `s.pi t` are only partially defined, on `s`. -/
50
def pi (s : Finset α) (t : ∀ a, Finset (β a)) : Finset (∀ a ∈ s, β a) :=
0 commit comments