instIsTransBoundedFormula

Mathlib.ModelTheory.Equivalence

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

English

Another form of transitivity for Iff on bounded formulas under T.

Русский

Еще одна форма транситивности для Iff над ограниченными формулами в рамках T.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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