fun_star — Mathlib

English

If f =^l g, then star f =^l star g for functions into a Star object.

Русский

Если f =^l g, то star f =^l star g для функций в Star-объекте.

LaTeX

$$$\\\\forall R \\\\ [Star R], \\\\forall f,g : \\\\alpha \\\\to R, \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\ (f =^l g) \\\\Rightarrow \\\\ (star \\\\circ f) =^l (star \\\\circ g)$$$

Lean4

protected theorem fun_star {R : Type*} [Star R] {f g : α → R} {l : Filter α} (h : f =ᶠ[l] g) :
    (fun x ↦ star (f x)) =ᶠ[l] fun x ↦ star (g x) :=
  h.fun_comp Star.star

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