exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating

English

If there is a separating family on univ (the whole space) under p with a separating condition hl for p, there exists a singleton {a} in the filter l contained in s.

Русский

Если существует разделяющее семейство на все множество под p, с условием hl, то существует элемент a такой что {a} находится в фильтре l.

LaTeX

$$$$\\exists a \\in s, \\{a\\} \\in l.$$$$

Lean4

theorem exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating (p : Set α → Prop) {s : Set α}
    [HasCountableSeparatingOn α p s] (hs : s ∈ l) (hne : s.Nonempty) (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) :
    ∃ a ∈ s, { a } ∈ l :=
  by
  rcases exists_subset_subsingleton_mem_of_forall_separating p hs hl with ⟨t, hts, ht, htl⟩
  rcases ht.eq_empty_or_singleton with rfl | ⟨x, rfl⟩
  · exact hne.imp fun a ha ↦ ⟨ha, mem_of_superset htl (empty_subset _)⟩
  · exact ⟨x, hts rfl, htl⟩

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