forall_prop_congr' — Mathlib

English

For any p, p' and q, q' as above, the equality (∀ h, q h) = ∀ h: p', q'(hp.2 h) holds when hq/hp are as in the previous lemma.

Русский

Для любых p, p' и q, q' справедлива равенство (∀ h, q h) = ∀ h: p', q'(hp.2 h).

LaTeX

$$$(\forall h, q(h)) = (\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) :=
  propext (forall_prop_congr hq hp)

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