Imp — Mathlib

English

If φ implies θ and ψ implies θ (in all models of T), then φ ⊔ ψ implies θ.

Русский

Если φ обусловливает θ и ψ обусловливает θ в моделях T, то φ ∨ ψ обусловливает θ.

LaTeX

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

Lean4

/-- `φ ⟹[T] ψ` indicates that `φ` implies `ψ` in models of `T`. -/
protected def Imp (T : L.Theory) (φ ψ : L.BoundedFormula α n) : Prop :=
  T ⊨ᵇ φ.imp ψ

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