imp_inf_iff — Mathlib

English

The implication from φ to the conjunction ψ ⊓ θ is equivalent to φ ⟹[T] ψ and φ ⟹[T] θ.

Русский

Импликация φ → (ψ ∧ θ) эквивалентна φ ⟹[T] ψ и φ ⟹[T] θ.

LaTeX

$$$(φ ⟹[T] ψ ⊓ θ) \\iff (φ ⟹[T] ψ) ∧ (φ ⟹[T] θ)$$$

Lean4

theorem imp_inf_iff {φ ψ θ : L.BoundedFormula α n} : (φ ⟹[T] ψ ⊓ θ) ↔ (φ ⟹[T] ψ) ∧ (φ ⟹[T] θ) :=
  ⟨fun h => ⟨h.trans (inf_imp_left _ _), h.trans (inf_imp_right _ _)⟩, fun ⟨h₁, h₂⟩ => imp_inf h₁ h₂⟩

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