of_forall_separating_mem_iff — Mathlib

English

The equivalence between HasCountableSeparatingOn on the subtype and HasCountableSeparatingOn on α as stated by subtype_iff holds.

Русский

Эквивалентность между разделением на подтипе и на исходном множестве, сформулированная через subtype_iff, сохраняется.

LaTeX

$$$$\\text{HasCountableSeparatingOn } t^{\\mathrm{Elem}}(\\lambda u. \\exists v, p(v) \\land (\\{v\\} \\text{ preimage}) = u) \\; \\leftrightarrow \\; \\text{HasCountableSeparatingOn } \\alpha p t.$$$$

Lean4

theorem of_forall_separating_mem_iff (p : Set β → Prop) [HasCountableSeparatingOn β p univ]
    (h : ∀ U : Set β, p U → ∀ᶠ x in l, f x ∈ U ↔ g x ∈ U) : f =ᶠ[l] g :=
  of_eventually_mem_of_forall_separating_mem_iff p (s := univ) univ_mem univ_mem h

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