cfcₙ_map — Mathlib

English

For any f, a, cfc_n (λx, -(f x)) a = -(cfc_n f a).

Русский

Для любого f и a cfc_n (λx, -(f x)) a = -(cfc_n f a).

LaTeX

$$$$ cfc\\!_n(\\lambda x. -f(x))\\,a = -\\bigl(cfc\\!_n f\\,a\\bigr) $$$$

Lean4

@[simp]
instance cfcₙ_map (f : R → R) (a : A) : IsStarNormal (cfcₙ f a) where
  star_comm_self :=
    by
    refine cfcₙ_cases (fun x ↦ Commute (star x) x) _ _ (Commute.zero_right _) fun _ _ _ ↦ ?_
    simp only [Commute, SemiconjBy]
    rw [← cfcₙ_apply f a, ← cfcₙ_star, ← cfcₙ_mul .., ← cfcₙ_mul ..]
    congr! 2
    exact
      mul_comm _
        _
          -- The following two lemmas are just `cfcₙ_predicate`, but specific enough for the `@[simp]` tag.

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