English
If a separating family exists for p1 on t1, and every p1-set is also p2, and t2 ⊆ t1, then there exists a separating family for p2 on t2.
Русский
Если существует разделяющее семейство для p1 на t1, и каждый множество с p1 также удовлетворяет p2, а t2 ⊆ t1, тогда существует разделяющее семейство для p2 на t2.
LaTeX
$$$$\\text{If } [\\exists S, S\\text{ countable}, \\forall s\\in S,\; p_1(s), \\forall x\\in t_2, \\forall y\\in t_2, (\\forall s\\in S, x\\in s \\iff y\\in s) \\Rightarrow x=y] \\text{ and } t_2\\subseteq t_1, \\, (p_1\\Rightarrow p_2) \\Rightarrow \\text{HasCountableSeparatingOn } \\alpha p_2 t_2.$$$$
Lean4
theorem mono {α} {p₁ p₂ : Set α → Prop} {t₁ t₂ : Set α} [h : HasCountableSeparatingOn α p₁ t₁] (hp : ∀ s, p₁ s → p₂ s)
(ht : t₂ ⊆ t₁) : HasCountableSeparatingOn α p₂ t₂ where
exists_countable_separating :=
let ⟨S, hSc, hSp, hSt⟩ := h.1
⟨S, hSc, fun s hs ↦ hp s (hSp s hs), fun x hx y hy ↦ hSt x (ht hx) y (ht hy)⟩
