exists_eventuallyEq_const_of_eventually_mem_of_forall_separating

English

If a set of β-valued functions satisfy a separation property for all U with p(U) and there is some nonempty β, then there exists a constant function f ≡ a eventually.

Русский

Если множество функций со значениями β удовлетворяет разделяющему условию для всех U с p(U) и β ненулевого размера, тогда существует константная функция f ≡ a, которая эквивалентна на концах.

LaTeX

$$$$\\exists a, f =^{l} const_{α} a.$$$$

Lean4

theorem exists_eventuallyEq_const_of_eventually_mem_of_forall_separating [Nonempty β] (p : Set β → Prop) {s : Set β}
    [HasCountableSeparatingOn β p s] (hs : ∀ᶠ x in l, f x ∈ s)
    (h : ∀ U, p U → (∀ᶠ x in l, f x ∈ U) ∨ (∀ᶠ x in l, f x ∉ U)) : ∃ a, f =ᶠ[l] const α a :=
  exists_singleton_mem_of_mem_of_forall_separating (l := map f l) p hs h

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