symm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[symm]
protected theorem symm {φ ψ : L.BoundedFormula α n} (h : φ ⇔[T] ψ) : ψ ⇔[T] φ := fun M v xs =>
  by
  rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
  exact h M v xs

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