imp_sup_right

Mathlib.ModelTheory.Equivalence

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

← MathLib Explorer

English

If ψ ⟹[T] θ and φ ⟹[T] θ then ψ ⟹[T] max(φ, ψ) or similar.

Русский

Если ψ и φ ведут к θ, то ψ ⟹[T] max(φ, ψ) и т.д.

LaTeX

$$$T.\\mathrm{Imp}(ψ, θ) \\to T.\\mathrm{Imp}(φ, θ) \\to T.\\mathrm{Imp}(\\mathrm{max}(φ, ψ), θ)$$$

Lean4

theorem imp_sup_right (φ ψ : L.BoundedFormula α n) : ψ ⟹[T] φ ⊔ ψ := fun M v xs =>
  by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact Or.inr

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

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

Разделы

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

Аффилиация

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