of_eventually_mem_of_forall_separating_mem_iff

English

If there is a separating structure on β in terms of U and p(U), then f and g are equal if and only if all U preserve membership equivalence in f and g eventually.

Русский

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

LaTeX

$$$$f =_{l} g \\iff \\forall U, p(U) \\to (f \\in U \\iff g \\in U)$$$$

Lean4

theorem of_eventually_mem_of_forall_separating_mem_iff (p : Set β → Prop) {s : Set β}
    [h' : HasCountableSeparatingOn β p s] (hf : ∀ᶠ x in l, f x ∈ s) (hg : ∀ᶠ x in l, g x ∈ s)
    (h : ∀ U : Set β, p U → ∀ᶠ x in l, f x ∈ U ↔ g x ∈ U) : f =ᶠ[l] g :=
  by
  rcases h'.1 with ⟨S, hSc, hSp, hS⟩
  have H : ∀ᶠ x in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s := (eventually_countable_ball hSc).2 fun s hs ↦ (h _ (hSp _ hs))
  filter_upwards [H, hf, hg] with x hx hxf hxg using hS _ hxf _ hxg hx

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