nqed.
ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
ndefinition mm_counter_image:
nqed.
ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
ndefinition mm_counter_image: