imp_right

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#BAll.imp_right

English

If H : ∀ x h, P x h → Q x h and h₁ : ∀ x h, P x h, then ∀ x h, Q x h.

Русский

Если H : ∀ x h, P x h → Q x h и h₁ : ∀ x h, P x h, тогда ∀ x h, Q x h.

LaTeX

$$$(H : \forall x h, P x h \to Q x h) \to (h1 : \forall x h, P x h) \to \forall x h, Q x h$$

Lean4

theorem imp_right (H : ∀ x h, P x h → Q x h) (h₁ : ∀ x h, P x h) (x h) : Q x h :=
  H _ _ <| h₁ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru