iffSetoid

Mathlib.ModelTheory.Equivalence

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

← MathLib Explorer

English

If φ ⇔ ψ modulo T, then φ.ex ⇔ ψ.ex.

Русский

Если φ ⇔ ψ по отношению к T, то φ.ex ⇔ ψ.ex.

LaTeX

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

Lean4

/-- Semantic equivalence forms an equivalence relation on formulas. -/
def iffSetoid (T : L.Theory) : Setoid (L.BoundedFormula α n)
    where
  r := T.Iff
  iseqv := ⟨fun _ => refl _, fun {_ _} h => h.symm, fun {_ _ _} h1 h2 => h1.trans h2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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