mp

Mathlib.ModelTheory.Equivalence

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

English

From a T-equivalence φ ⇔ ψ, derive φ ⇒_T ψ.

Русский

Из эквивалентности φ ⇔_T ψ следует φ ⇒_T ψ.

LaTeX

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

Lean4

protected theorem mp {φ ψ : L.BoundedFormula α n} (h : φ ⇔[T] ψ) : φ ⟹[T] ψ :=
  (iff_iff_imp_and_imp.1 h).1

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

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

Разделы

Аффилиация

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