forall_and_index' — Mathlib

English

Let p and q be propositions and r : p → q → Prop. Then (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ h : p ∧ q, r h.1 h.2.

Русский

Пусть p, q — пропозиции, и r : p → q → Prop. Тогда (∀ (hp : p) (hq : q), r hp hq) эквивалентно ∀ h : p ∧ q, r h.1 h.2.

LaTeX

$$$(\forall (hp : p) (hq : q), r\, hp\, hq) \iff \forall h : p \land q, r(h.1)(h.2)$$$

Lean4

theorem forall_and_index' {p q : Prop} {r : p → q → Prop} : (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ h : p ∧ q, r h.1 h.2 :=
  (forall_and_index (r := fun h => r h.1 h.2)).symm

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