imp_inf — Mathlib

English

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

Русский

Если φ ⟹[T] ψ и φ ⟹[T] θ, то φ ⟹[T] ψ ⊓ θ.

LaTeX

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

Lean4

theorem imp_inf {φ ψ θ : L.BoundedFormula α n} (h₁ : φ ⟹[T] ψ) (h₂ : φ ⟹[T] θ) : φ ⟹[T] ψ ⊓ θ := fun M v xs =>
  by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

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