English
If a countable separating family exists on the subtype t with respect to q, and every U in t with q(U) can be traced back to some V in α with p(V) and the preimage of V equals U, then α has a countable separating family for p on t.
Русский
Если на подтипе t существует счетное разделяющее семейство относительно q, и каждому U ⊆ t с q(U) соответствует V ⊆ α с p(V) и preimage(V) = U, то α имеет счетное разделяющее семейство для p на t.
LaTeX
$$$$\\text{If } [h : HasCountableSeparatingOn t\\; q\\; univ],\\; (\\forall U, q(U) \\Rightarrow \\exists V, p(V) \\land (\\uparrow)^{-1}' V = U) \\Rightarrow HasCountableSeparatingOn \\alpha p t.$$$$
Lean4
theorem of_subtype {α : Type*} {p : Set α → Prop} {t : Set α} {q : Set t → Prop} [h : HasCountableSeparatingOn t q univ]
(hpq : ∀ U, q U → ∃ V, p V ∧ (↑) ⁻¹' V = U) : HasCountableSeparatingOn α p t :=
by
rcases h.1 with ⟨S, hSc, hSq, hS⟩
choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)
refine ⟨⟨V '' S, hSc.image _, forall_mem_image.2 hpV, fun x hx y hy h ↦ ?_⟩⟩
refine congr_arg Subtype.val (hS ⟨x, hx⟩ trivial ⟨y, hy⟩ trivial fun U hU ↦ ?_)
rw [← hV U hU]
exact h _ (mem_image_of_mem _ hU)
