Skip to content

Commit

Permalink
fix: missing word overlaps our -> overlaps with our
Browse files Browse the repository at this point in the history
  • Loading branch information
extradosages authored and PatrickMassot committed Dec 22, 2023
1 parent 8040702 commit ddbc586
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion MIL/C07_Hierarchies/S03_Subobjects.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Sub-objects
After defining some algebraic structure and its morphisms, the next step is to consider sets
that inherit this algebraic structure, for instance subgroups or subrings.
This largely overlaps our previous topic. Indeed a set in ``X`` is implemented as a function from
This largely overlaps with our previous topic. Indeed a set in ``X`` is implemented as a function from
``X`` to ``Prop`` so sub-objects are function satisfying a certain predicate.
Hence we can reuse of lot of the ideas that led to the ``FunLike`` class and its descendants.
We won't reuse ``FunLike`` itself because this would break the abstraction barrier from ``Set X``
Expand Down

0 comments on commit ddbc586

Please sign in to comment.