forall_and_index — Mathlib

English

Let p and q be propositions and r a function on p ∧ q. Then (∀ h : p ∧ q, r h) ↔ ∀ (hp : p) (hq : q), r ⟨hp, hq⟩.

Русский

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

LaTeX

$$$\forall h : (p \land q), r(h) \;\iff\; \forall (hp : p) (hq : q), r (\langle hp, hq \rangle)$$$

Lean4

@[simp]
theorem forall_and_index {p q : Prop} {r : p ∧ q → Prop} : (∀ h : p ∧ q, r h) ↔ ∀ (hp : p) (hq : q), r ⟨hp, hq⟩ :=
  ⟨fun h hp hq ↦ h ⟨hp, hq⟩, fun h h1 ↦ h h1.1 h1.2⟩

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