English
HasCountableSeparatingOn t with a certain existential lifting to α is equivalent to HasCountableSeparatingOn α p t.
Русский
Имеемое на подтипе t разделяющее свойство с существующим переносом во множество α эквивалентно наличию разделяющего свойства на α с p.
LaTeX
$$$$HasCountableSeparatingOn\\ t\\ (\\lambda u. \\exists v, p(v) \\land (\\operatorname{preimage} \\operatorname{Subtype.val} v) = u)\\ univ \\; \\iff\\; HasCountableSeparatingOn\\ alpha\\ p\\ t.$$$$
Lean4
theorem subtype_iff {α : Type*} {p : Set α → Prop} {t : Set α} :
HasCountableSeparatingOn t (fun u ↦ ∃ v, p v ∧ (↑) ⁻¹' v = u) univ ↔ HasCountableSeparatingOn α p t :=
by
constructor <;> intro h
· exact h.of_subtype <| fun s ↦ id
rcases h with ⟨S, Sct, Sp, hS⟩
use {Subtype.val ⁻¹' s | s ∈ S}, Sct.image _, ?_, ?_
· rintro u ⟨t, tS, rfl⟩
exact ⟨t, Sp _ tS, rfl⟩
rintro x - y - hxy
exact
Subtype.val_injective <|
hS _ (Subtype.coe_prop _) _ (Subtype.coe_prop _) fun s hs ↦ hxy (Subtype.val ⁻¹' s) ⟨s, hs, rfl⟩
