English
For a predicate r on pairs of α, LiftR r x y holds iff there exist a, f0, f1 with x = ⟨a, f0⟩, y = ⟨a, f1⟩ and ∀ i j, r (f0 i j) (f1 i j).
Русский
Пусть r — отношение на пары α; тогда LiftR r x y эквивалентно существованию a, f0, f1 с x = ⟨a, f0⟩, y = ⟨a, f1⟩ и ∀ i j, r (f0 i j) (f1 i j).
LaTeX
$$$\\text{LiftR } r\\, x\\, y \\;\\Longleftrightarrow\\; \\exists a\\, f_0\\, f_1,\\ x = \\langle a, f_0 \\rangle \\land y = \\langle a, f_1 \\rangle \\land \\forall i j, r (f_0 i j) (f_1 i j)$$$
Lean4
theorem liftR_iff {α : TypeVec n} (r : ∀ ⦃i⦄, α i → α i → Prop) (x y : P α) :
LiftR (@r) x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ i j, r (f₀ i j) (f₁ i j) :=
by
constructor
· rintro ⟨u, xeq, yeq⟩
rcases h : u with ⟨a, f⟩
use a, fun i j => (f i j).val.fst, fun i j => (f i j).val.snd
constructor
· rw [← xeq, h]
rfl
constructor
· rw [← yeq, h]
rfl
intro i j
exact (f i j).property
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
use ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩
dsimp; constructor
· rw [xeq]
rfl
rw [yeq]; rfl
