trans

Mathlib.ModelTheory.Equivalence

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

← MathLib Explorer

English

If φ ⟹[T] ψ and ψ ⟹[T] θ then φ ⟹[T] θ.

Русский

Если φ следует от T к ψ и ψ следует от T к θ, то φ следует от T к θ.

LaTeX

$$$(φ ⟹[T] ψ) \\land (ψ ⟹[T] θ) \\Rightarrow (φ ⟹[T] θ)$$$

Lean4

@[trans]
protected theorem trans {φ ψ θ : L.BoundedFormula α n} (h1 : φ ⟹[T] ψ) (h2 : ψ ⟹[T] θ) : φ ⟹[T] θ := fun M v xs =>
  (h2 M v xs) ∘ (h1 M v xs)

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

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

Разделы

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

Аффилиация

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