instIsSymmBoundedFormula

Mathlib.ModelTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.Iff.instIsSymmBoundedFormula

English

Iff is symmetric for all φ, ψ; the symmetric property holds as a structural instance.

Русский

Симметричность Iff следует как структурный инстанс для любых формул.

LaTeX

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

Lean4

instance : IsSymm (L.BoundedFormula α n) T.Iff :=
  ⟨fun _ _ => Iff.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru