iff_iff_imp_and_imp — Mathlib

English

Let φ and ψ be formulas in the language bounded by T. They are equivalent modulo T if and only if φ implies ψ modulo T and ψ implies φ modulo T.

Русский

Пусть φ и ψ — формулы в языке; они эквивалентны по теории T тогда и только тогда, когда φ следует из ψ по отношению к T и ψ следует из φ по отношению к T.

LaTeX

$$$$ (\varphi \iff_T \psi) \iff (\varphi \Rightarrow_T \psi) \wedge (\psi \Rightarrow_T \varphi) $$$$

Lean4

theorem iff_iff_imp_and_imp {φ ψ : L.BoundedFormula α n} : (φ ⇔[T] ψ) ↔ (φ ⟹[T] ψ) ∧ (ψ ⟹[T] φ) := by
  simp only [Theory.Imp, ModelsBoundedFormula, BoundedFormula.realize_imp, ← forall_and, Theory.Iff,
    BoundedFormula.realize_iff, iff_iff_implies_and_implies]

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