exists_subsingleton_mem_of_forall_separating

English

Under CountableInterFilter l, for a p with HasCountableSeparatingOn on univ, there exists a subsingleton subset t of s such that t ∈ l.

Русский

При CountableInterFilter l существует subsingleton подмножество t ⊆ s такое, что t ∈ l.

LaTeX

$$$$\\exists t, t \\subseteq s \\land t.Subsingleton \\land t \\in l.$$$$

Lean4

theorem exists_subsingleton_mem_of_forall_separating (p : Set α → Prop) [HasCountableSeparatingOn α p univ]
    (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) : ∃ s : Set α, s.Subsingleton ∧ s ∈ l :=
  let ⟨t, _, hts, htl⟩ := exists_subset_subsingleton_mem_of_forall_separating p univ_mem hl
  ⟨t, hts, htl⟩

Похожие утверждения