What is the standard Set package or import

Stream: general

[Mason McBride]

I'm interested as to why there seems to be different definitions of a set like 'Set' and 'set' and 'Setoid' and 'finset' which one should I be using? What is the history?

[Mario Carneiro]

Note, the lowercased names no longer exist, those look like they are from the lean 3 naming convention

[Mario Carneiro]

The lean 4 version of those would be ZFSet, Set, Setoid, Finset respectively

[Mario Carneiro]

• Set A: an arbitrary subset of base type A
• Finset A: a finite set (with some computational content as a list of elements)
• Setoid A: an equivalence relation on a type (this isn't really a set, the naming is borrowed from Coq)
• ZFSet: a ZFC-style set for use in set theory formalization

[Mario Carneiro]

you pretty much always want the first one, unless you are doing summation over finite sets in which case you will need the second one

[Mason McBride]

import Mathlib.Init.Set
set_option autoImplicit false
universe u

variable (α : Type u) (X Y Z : Set α)
theorem please (f: X → Y) (g: Y → Z) : Set.image (f ∘ g) = Set.image f ∘ Set.image g := by rfl

What is wrong here

[Ruben Van de Velde]

1. You're not importing enough of mathlib for lean to know what you mean when you try to use a set where a type of expected
2. You've got the order wrong for the composition operator
3. The proof needs more work

[Eric Wieser]

4. It looks like you're muddling Set and Type