English
A variant of liftp_iff that uses a representation u = ⟨a,f⟩ with f : α-type structure and asserts equivalence with existence of u and abs u = x and p on all coordinates.
Русский
Вариант liftp_iff' использует представление u = ⟨a,f⟩ и утверждает эквивалентность существованию u, abs u = x и p на всех координатах.
LaTeX
$$$\\\\mathrm{Liftp} p x \\\\equiv \\\\exists u : q.P α, abs\,u = x \\\\wedge \\\\forall i, p (u.snd i).$$$
Lean4
theorem liftp_iff' {α : Type u} (p : α → Prop) (x : F α) : Liftp p x ↔ ∃ u : q.P α, abs u = x ∧ ∀ i, p (u.snd i) :=
by
constructor
· rintro ⟨y, hy⟩
rcases h : repr y with ⟨a, f⟩
use ⟨a, fun i => (f i).val⟩
dsimp
constructor
· rw [← hy, ← abs_repr y, h, ← abs_map]
rfl
intro i
apply (f i).property
rintro ⟨⟨a, f⟩, h₀, h₁⟩; dsimp at *
use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
rw [← abs_map, ← h₀]; rfl
