sup_imp — Mathlib

English

The implication with a maximum of φ and ψ is equivalent to conjunction of φ ⟹ θ and ψ ⟹ θ.

Русский

Импликация через максимум φ и ψ эквивалентна сочетанию φ ⟹ θ и ψ ⟹ θ.

LaTeX

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

Lean4

theorem sup_imp {φ ψ θ : L.BoundedFormula α n} (h₁ : φ ⟹[T] θ) (h₂ : ψ ⟹[T] θ) : φ ⊔ ψ ⟹[T] θ := fun M v xs =>
  by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact fun h => h.elim (h₁ M v xs) (h₂ M v xs)

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