exists_singleton_mem_of_mem_of_forall_separating

English

If there exists a nonempty set s with HasCountableSeparatingOn α p s and hl as in the hypothesis, then there exists a ∈ s with {a} ∈ l.

Русский

Если существует непустое s с разделяющим свойством HasCountableSeparatingOn α p s, тогда найдётся a ∈ s такое, что {a} ∈ l.

LaTeX

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

Lean4

theorem exists_singleton_mem_of_mem_of_forall_separating [Nonempty α] (p : Set α → Prop) {s : Set α}
    [HasCountableSeparatingOn α p s] (hs : s ∈ l) (hl : ∀ U, p U → U ∈ l ∨ Uᶜ ∈ l) : ∃ a, { a } ∈ l :=
  by
  rcases s.eq_empty_or_nonempty with rfl | hne
  · exact ‹Nonempty α›.elim fun a ↦ ⟨a, mem_of_superset hs (empty_subset _)⟩
  · exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦ And.right

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