rel_exists — Mathlib

English

Let R be BiTotal. Then an existential lifting through implication holds: ((R ⇒ Iff) ⇒ Iff) (fun p => ∃ i, p i) (fun q => ∃ i, q i).

Русский

Пусть R — BiTotal. Тогда существование распространяется через импликацию с эквивалентностью: (R ⇒ Iff) ⇒ Iff применимо к ∃ i, p i и ∃ i, q i.

LaTeX

$$$((R \\Rightarrow Iff) \\Rightarrow Iff) (\\\\lambda p. \\\\exists i, p i) (\\\\lambda q. \\\\exists i, q i)$$$

Lean4

theorem rel_exists (h : BiTotal R) : ((R ⇒ Iff) ⇒ Iff) (fun p => ∃ i, p i) (fun q => ∃ i, q i) := fun _ _ Hrel =>
  ⟨fun ⟨a, pa⟩ => (h.left a).imp fun _ Rab => (Hrel Rab).1 pa, fun ⟨b, qb⟩ =>
    (h.right b).imp fun _ Rab => (Hrel Rab).2 qb⟩

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