head_supports — Mathlib

English

If q is S-supported, then for every k, the state head k q is also S-supported.

Русский

Если q поддерживается S, то для любого k состояние head k q тоже поддерживается S.

LaTeX

$$$\\forall S,\\forall k,\\forall q,\\ (q \\text{ is S-supported}) \\Rightarrow (\\mathrm{head}\\ k\\ q) \\text{ is S-supported}.$$$

Lean4

theorem head_supports {S k q} (H : (q : Λ').Supports S) : (head k q).Supports S := fun _ => by dsimp only;
  split_ifs <;> exact H

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