imp_antisymm — Mathlib

English

If φ implies ψ and ψ implies φ modulo T, then φ is equivalent to ψ modulo T.

Русский

Если φ следует из ψ и ψ следует из φ по отношению к T, то φ эквивалентно ψ по отношению к T.

LaTeX

$$$$ (\varphi \Rightarrow_T \psi) \land (\psi \Rightarrow_T \varphi) \Rightarrow (\varphi \iff_T \psi) $$$$

Lean4

theorem imp_antisymm {φ ψ : L.BoundedFormula α n} (h₁ : φ ⟹[T] ψ) (h₂ : ψ ⟹[T] φ) : φ ⇔[T] ψ :=
  iff_iff_imp_and_imp.2 ⟨h₁, h₂⟩

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