English
Let R be BiTotal. Then a lifting of Iff to universal quantification is an equivalence between ∀ i, p i and ∀ i, q i whenever p i ↔ q i holds pointwise.
Русский
Пусть R — BiTotal. Тогда отображение, переводящее p i в ∀ i p i, образует эквивалентность между ∀ i p i и ∀ i q i, если p i ↔ q i по каждому i.
LaTeX
$$$\\\\operatorname{Relator.LiftFun} (\\\\operatorname{Relator.LiftFun} R Iff) Iff (fun p => \\\\forall i, p i) (fun q => \\\\forall i, q i)$$$
Lean4
theorem rel_forall (h : BiTotal R) : ((R ⇒ Iff) ⇒ Iff) (fun p => ∀ i, p i) (fun q => ∀ i, q i) := fun _ _ Hrel =>
⟨fun H b => Exists.elim (h.right b) (fun _ Rab => (Hrel Rab).mp (H _)), fun H a =>
Exists.elim (h.left a) (fun _ Rab => (Hrel Rab).mpr (H _))⟩
