English
If there exist γ and injections as described such that every β comes from an α via f and g, then β is Small.
Русский
Если существует γ и отображения, которые связывают β через f и g с α, и каждый β встречается как g b = f a, то β мала.
LaTeX
$$$ \\forall f,g, \\text{Injective}(g) \\rightarrow (\\forall b, \\exists a, f(a) = g(b)) \\Rightarrow \\text{Small}(\\beta) $$$
Lean4
/-- This can be seen as a version of `small_of_surjective` in which the function `f` doesn't
actually land in `β` but in some larger type `γ` related to `β` via an injective function `g`.
-/
theorem small_of_injective_of_exists {α : Type v} {β : Type w} {γ : Type v'} [Small.{u} α] (f : α → γ) {g : β → γ}
(hg : Function.Injective g) (h : ∀ b : β, ∃ a : α, f a = g b) : Small.{u} β :=
by
by_cases hβ : Nonempty β
· refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)
obtain ⟨a, ha⟩ := h b
exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩
· simp only [not_nonempty_iff] at hβ
infer_instance
