cfcₙ_commute_cfcₙ — Mathlib

English

If the predicate p fails for a, then cfcₙ f a = 0.

Русский

Если предикат p не выполняется для a, то cfcₙ f a = 0.

LaTeX

$$Not (p a) → cfcₙ f a = 0$$

Lean4

theorem cfcₙ_commute_cfcₙ (f g : R → R) (a : A) : Commute (cfcₙ f a) (cfcₙ g a) :=
  by
  refine cfcₙ_cases (fun x ↦ Commute x (cfcₙ g a)) a f (by simp) fun hf hf0 ha ↦ ?_
  refine cfcₙ_cases (fun x ↦ Commute _ x) a g (by simp) fun hg hg0 _ ↦ ?_
  exact Commute.all _ _ |>.map _

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