Fix a fix

avigad · Dec 22, 2023 · bc3647f · bc3647f
1 parent a400dc3
commit bc3647f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
@@ -129,7 +129,7 @@ and returns an arbitrary element of ``β`` otherwise.
 The function ``invFun g`` is always a left inverse if ``g`` is injective
 and a right inverse if ``g`` is surjective.
 
--- LITERALINCLUDE: inv_fun g
+-- LITERALINCLUDE: invFun g
 
 We define the set corresponding to the union of the shaded regions as follows.