forall_prop_congr — Mathlib

English

If hq : ∀ h, q h ↔ q' h and hp : p ↔ p', then (∀ h, q h) ↔ ∀ h: p', q'(hp.2 h).

Русский

Если hq : ∀ h, q h ↔ q' h и hp : p ↔ p', то (∀ h, q h) ↔ ∀ h: p', q'(hp.2 h).

LaTeX

$$$(\forall h, q(h)) \iff (\forall h : p', q'(hp.2(h)))$$$

Lean4

theorem forall_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) ↔ ∀ h : p', q' (hp.2 h) :=
  ⟨fun h1 h2 ↦ (hq _).1 (h1 (hp.2 h2)), fun h1 h2 ↦ (hq _).2 (h1 (hp.1 h2))⟩

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