English
sigmaImp encodes the logical connective implication for pairs of bounded formulas by aligning their bounds when equal, otherwise yielding an undefined value.
Русский
sigmaImp кодирует логическое следование импликации для пары ограниченных формул, приводя к одинаковым границам или к неопределённости.
LaTeX
$$$\\sigmaImp: (\\Sigma n, L.BoundedFormula\\,\\alpha\\, n) \\to (\\Sigma n, L.BoundedFormula\\,\\alpha\\, n) \\to (\\Sigma n, L.BoundedFormula\\,\\alpha\\, n)$, \\\\sigmaImp(⟨m, \\varphi⟩, ⟨n, \\psi⟩) = \\begin{cases} ⟨m, \\varphi.imp(\\psi)⟩ & \\text{if } m = n, \\\\ \\text{default} & \\text{otherwise}. \\end{cases}$$$
Lean4
/-- Applies `imp` to two elements of `(Σ n, L.BoundedFormula α n)`,
or returns `default` if not possible. -/
def sigmaImp : (Σ n, L.BoundedFormula α n) → (Σ n, L.BoundedFormula α n) → Σ n, L.BoundedFormula α n
| ⟨m, φ⟩, ⟨n, ψ⟩ => if h : m = n then ⟨m, φ.imp (Eq.mp (by rw [h]) ψ)⟩ else default
