English
Under CountableInterFilter l and HasCountableSeparatingOn α p s, if every U with p(U) is in l or its complement is in l, there exists a subset t of s which is a subsingleton and belongs to l.
Русский
При наличии CountableInterFilter l и HasCountableSeparatingOn α p s, если для каждого U с p(U) верно U∈l или U^c∈l, существует подмножество t ⊆ s, образующее subsingleton и принадлежащее l.
LaTeX
$$$$\\exists t \\subseteq s,\\ t\\text{ Subs singleton} \\land t\\in l.$$$$
Lean4
theorem exists_subset_subsingleton_mem_of_forall_separating (p : Set α → Prop) {s : Set α}
[h : HasCountableSeparatingOn α p s] (hs : s ∈ l) (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) :
∃ t, t ⊆ s ∧ t.Subsingleton ∧ t ∈ l := by
rcases h.1 with ⟨S, hSc, hSp, hS⟩
refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
· exact fun _ h ↦ h.1.1
· intro x hx y hy
simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy
refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)
cases hl s (hSp s hsS) with
| inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
| inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
·
exact
inter_mem (inter_mem hs ((countable_sInter_mem (hSc.mono inter_subset_left)).2 fun _ h ↦ h.2))
((countable_bInter_mem hSc).2 fun U hU ↦ iInter_mem'.2 id)
