Inductive creates a new type and gives it a name. It is similar to datatype in SML, data in Haskell, type (defining an ordinary variant or a record) in Ocaml.
In addition to defining the type, Inductive also defines induction principles for that type. These induction principles aren't necessary from a theoretical point of view: all they do is to give a name to a particular well-typed term. They are provided because while you could write that term in your proof, it is mechanical and repetitive.
Definition gives a name to a term. It's broadly similar to let in SML or Ocaml or Haskell (but it doesn't let you write recursive definitions as such). Since Coq is pure (no side effects), if you write two definitions with the same right-hand side, the resulting names are equal. You can use Definition at any level of the sort hierarchy, including for types (in which case the definition is similar to type aliases in SML, Ocaml or Haskell).
Fixpoint is similar to Definition, but allows a recursive definition (like let rec in ML). It's in fact syntactic sugar for Definition plus the explicit fixpoint combinator fix, but definitions made using Fixpoint are easier to read and write.
The best way to understand these is to write a few proofs about some datatype. Try to rewrite some parts of the List library, for example.
There are several ways to implement finite sets in Coq. To to set theory proofs, try Sets.Finite_sets. If you want to have decent extracted code, use MSets.MSetAVL.
:and:=have different meanings in different contexts. $\endgroup$