fun_comp — Mathlib

English

If f =^l g, then h ∘ f =^l h ∘ g for any function h.

Русский

Если f =^l g, то h ∘ f =^l h ∘ g для любой функции h.

LaTeX

$$$\\\\forall f,g \\\\in \\\\alpha \\\\to \\\\beta, \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall h \\\\in (\\\\beta \\\\to \\\\gamma), \\\\ (f =^l g) \\\\Rightarrow \\\\ (h \\\\circ f) =^l (h \\\\circ g)$$$

Lean4

theorem fun_comp {f g : α → β} {l : Filter α} (H : f =ᶠ[l] g) (h : β → γ) : h ∘ f =ᶠ[l] h ∘ g :=
  H.mono fun _ hx => congr_arg h hx

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