English
The liftr relation between x and y in F α is equivalent to the existence of a shared representation a and f0,f1 of x,y such that x=abs ⟨a,f0⟩, y=abs ⟨a,f1⟩, and r on all coordinates holds.
Русский
Связь liftr между x и y в F α эквивалентна существованию общей репрезентации a и f0,f1 such что x=abs ⟨a,f0⟩, y=abs ⟨a,f1⟩ и для всех координат выполняется отношение r между f0_i и f1_i.
LaTeX
$$$\\\\ Liftr r x y \\\\iff \\\\exists a f_0 f_1, x = abs ⟨a,f_0⟩ \\\\wedge y = abs ⟨a,f_1⟩ \\\\wedge \\forall i, r (f_0 i) (f_1 i).$$$
Lean4
theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : F α) :
Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i) :=
by
constructor
· rintro ⟨u, xeq, yeq⟩
rcases h : repr u with ⟨a, f⟩
use a, fun i => (f i).val.fst, fun i => (f i).val.snd
constructor
· rw [← xeq, ← abs_repr u, h, ← abs_map]
rfl
constructor
· rw [← yeq, ← abs_repr u, h, ← abs_map]
rfl
intro i
exact (f i).property
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
constructor
· rw [xeq, ← abs_map]
rfl
rw [yeq, ← abs_map]; rfl
