preimage — Mathlib

English

If f =^l g then for any s, f^{-1}(s) =^l g^{-1}(s).

Русский

Если f =^l g, то для любого множества s выполняется f^{-1}(s) =^l g^{-1}(s).

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall f,g : \\\\alpha \\\\to β, \\\\ (f =^l g) \\\\Rightarrow \\\\forall s \\\\subseteq β, \\\\bigl(f^{-1}' s =^l g^{-1}' s\\\\bigr)$$$

Lean4

@[gcongr]
theorem preimage {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (s : Set β) : f ⁻¹' s =ᶠ[l] g ⁻¹' s :=
  h.fun_comp s

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