sigmaImp_apply — Mathlib

English

Decodes a pair of bounded formulas with the same bound by interpreting the encoded pair as their implication.

Русский

Декодирует пару ограниченных формул с одинаковой границей и интерпретирует закодированную пару как их импликацию.

LaTeX

$$$\\sigmaImp(⟨n, φ⟩, ⟨n, ψ⟩) = ⟨n, φ.imp ψ⟩$$$

Lean4

/-- Decodes a list of symbols as a list of formulas. -/
@[simp]
theorem sigmaImp_apply {n} {φ ψ : L.BoundedFormula α n} : sigmaImp ⟨n, φ⟩ ⟨n, ψ⟩ = ⟨n, φ.imp ψ⟩ := by
  simp only [sigmaImp, ↓reduceDIte, eq_mp_eq_cast, cast_eq]

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