doc(docs/overview.yaml): Added Hall's theorem (#6205)

Also fixed module documentation to use inline math mode (and removed the dreaded "any").

docs/overview.yaml

@@ -326,6 +326,8 @@ Combinatorics:
     finite: 'fintype.exists_ne_map_eq_of_card_lt'
     infinite: 'fintype.exists_infinite_fiber'
     strong pigeonhole principle: 'fintype.exists_lt_card_fiber_of_mul_lt_card'
+  Transversals:
+    Hall's marriage theorem: 'finset.all_card_le_bUnion_card_iff_exists_injective'
 
 Dynamics:
   Circle dynamics:

src/combinatorics/hall.lean

@@ -10,11 +10,11 @@ import data.set.finite
 /-!
 # Hall's Marriage Theorem
 
-Given a list of finite subsets $$X_1,X_2,\dots,X_n$$ of some given set
-$$S$$, Hall in [Hall1935] gave a necessary and sufficient condition
-for there to be a list of distinct elements $$x_1,x_2,\dots,x_n$$ with
-$$x_i\in X_i$$ for each $$i$$: it is when the union of any $$k$$ of
-these subsets has at least $$k$$ elements.
+Given a list of finite subsets $X_1,X_2,\dots,X_n$ of some given set
+$S$, Hall in [Hall1935] gave a necessary and sufficient condition for
+there to be a list of distinct elements $x_1,x_2,\dots,x_n$ with
+$x_i\in X_i$ for each $i$: it is when for each $k$, the union of every
+$k$ of these subsets has at least $k$ elements.
 
 This file proves this for an indexed family `t : ι → finset α` of
 finite sets, with `[fintype ι]`, along with some variants of the