English
LiftR has a similar characterization as LiftP, but for relations: it holds iff there exist a representation abovely equating x and y via abs ⟨a,f0⟩ and abs ⟨a,f1⟩ with a bound on r.
Русский
LiftR имеет аналогичную характеристику, но для отношений: оно эквивалентно тому, что существуют представления x = abs ⟨a,f0⟩ и y = abs ⟨a,f1⟩ с ограничением на r.
LaTeX
$$$$ \\mathrm{LiftR}\\; r\\; x\\; y \\;\\iff\\; \\exists a,f_0,f_1,\\; x = \\mathrm{abs}\\langle a,f_0\\rangle \\land y = \\mathrm{abs}\\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 : F α) :
LiftR r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ i j, r (f₀ i j) (f₁ i j) :=
by
constructor
· rintro ⟨u, xeq, yeq⟩
rcases h : repr 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, ← abs_repr u, h, ← abs_map]; rfl
constructor
· rw [← yeq, ← abs_repr u, h, ← abs_map]; rfl
intro i j
exact (f i j).property
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
use abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), h i j⟩⟩
dsimp; constructor
· rw [xeq, ← abs_map]; rfl
rw [yeq, ← abs_map]; rfl
