imp — Mathlib

English

If P implies Q for every element a, then for any tree t, All P t implies All Q t.

Русский

Если для каждого элемента a выполняется P(a) → Q(a), то для любого дерева t из All P t следует All Q t.

LaTeX

$$((\forall a, P a \Rightarrow Q a) \Rightarrow \forall t, All P t \Rightarrow All Q t)$$

Lean4

theorem imp {P Q : α → Prop} (H : ∀ a, P a → Q a) : ∀ {t}, All P t → All Q t
  | nil, _ => ⟨⟩
  | node _ _ _ _, ⟨h₁, h₂, h₃⟩ => ⟨h₁.imp H, H _ h₂, h₃.imp H⟩

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