of_forall_separating_preimage — Mathlib

English

If for every U with p(U) we have that the preimages under f and g coincide eventually for U, then f and g are eventually equal.

Русский

Если для каждого U с p(U) имеют место совпадения предобразов f и g в пределе, то f и g равны на пределе.

LaTeX

$$$$\\forall U, p(U) \\to f^{-1}(U) =_{l} g^{-1}(U) \\Rightarrow f =_{l} g.$$$$

Lean4

theorem of_forall_separating_preimage (p : Set β → Prop) [HasCountableSeparatingOn β p univ]
    (h : ∀ U : Set β, p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) : f =ᶠ[l] g :=
  of_eventually_mem_of_forall_separating_preimage p (s := univ) univ_mem univ_mem h

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