imp — Mathlib

English

If T equivalence holds for two pairs, then their implications are equivalent modulo T.

Русский

Если эквивалентность двоек формул удержана по отношению к T, то импликации между ними эквивалентны по T.

LaTeX

$$$$ (\varphi \iff_T \psi) \to (\varphi' \iff_T \psi') \to (\varphi.\text{imp } \varphi' \iff_T \psi.\text{imp } \psi') $$$$

Lean4

protected theorem imp {φ ψ φ' ψ' : L.BoundedFormula α n} (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
    (φ.imp φ') ⇔[T] (ψ.imp ψ') :=
  by
  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_imp]
  exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff

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