star — Mathlib

English

If f =^l g, then star f =^l star g for protected star mapping.

Русский

Если f =^l g, то star f =^l star g для защищённого отображения star.

LaTeX

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

Lean4

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

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