I cannot find A !=set0 -> f @` A !=set0 , which is quite a simple lemma. It seems like only the converse is in the classical_sets file.
A !=set0 -> f @` A !=set0
classical_sets
Last updated: Feb 05 2023 at 15:03 UTC