English
If a function f has a partial inverse g and the image f''s is finite, then s is finite.
Русский
Если существует частичный обратный g к f и образ f(s) конечен, то s конечно.
LaTeX
$$$\\forall s\\subseteq \\alpha,\\; (\\exists g\\, f,g \\text{IsPartialInv } f g) \\Rightarrow (\\operatorname{Finite}(f''s) \\Rightarrow \\operatorname{Finite}(s)).$$$
Lean4
/-- If a function `f` has a partial inverse `g` and the image of `s` under `f` is a set with
a `Fintype` instance, then `s` has a `Fintype` structure as well. -/
def fintypeOfFintypeImage (s : Set α) {f : α → β} {g} (I : IsPartialInv f g) [Fintype (f '' s)] : Fintype s :=
Fintype.ofFinset ⟨_, (f '' s).toFinset.2.filterMap g <| injective_of_isPartialInv_right I⟩ fun a =>
by
suffices (∃ b x, f x = b ∧ g b = some a ∧ x ∈ s) ↔ a ∈ s by
simpa [exists_and_left.symm, and_comm, and_left_comm, and_assoc]
rw [exists_swap]
suffices (∃ x, x ∈ s ∧ g (f x) = some a) ↔ a ∈ s by simpa [and_comm, and_left_comm, and_assoc]
simp [I _, (injective_of_isPartialInv I).eq_iff]
