Closed jkingdon closed 3 weeks ago
This proof turns out to be quite similar to https://us.metamath.org/ileuni/trilpo.html and in fact can use many of the same lemmas.
Includes iswomninn which is similar to isomninn but for weak omniscience (including lemma iswomninnlem ).
iswomninn
isomninn
iswomninnlem
Includes enwomni which says that weak omniscience is invariant with respect to equinumerosity.
enwomni
Fixes #4041
This proof turns out to be quite similar to https://us.metamath.org/ileuni/trilpo.html and in fact can use many of the same lemmas.
Includes
iswomninnwhich is similar toisomninnbut for weak omniscience (including lemmaiswomninnlem).Includes
enwomniwhich says that weak omniscience is invariant with respect to equinumerosity.Fixes #4041