supportsStmt_read — Mathlib

English

If every a has SupportsStmt S (f a), then SupportsStmt S (read dec f).

Русский

Если для каждого a выполняется SupportsStmt S (f a), то SupportsStmt S (read dec f).

LaTeX

$$supportsStmt_read (S) (dec) (f) (hf) : SupportsStmt S (read dec f)$$

Lean4

theorem supportsStmt_read {S : Finset (Λ' Γ Λ σ)} :
    ∀ {f : Γ → Stmt Bool (Λ' Γ Λ σ) σ}, (∀ a, SupportsStmt S (f a)) → SupportsStmt S (read dec f) :=
  suffices
    ∀ (i) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ), (∀ v, SupportsStmt S (f v)) → SupportsStmt S (readAux i f)
    from fun hf ↦ this n _ (by intro; simp only [supportsStmt_move, hf])
  fun i f hf ↦ by
  induction i with
  | zero => exact hf _
  | succ i IH => constructor <;> apply IH <;> intro <;> apply hf

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