English
Given a property p on α and an F-structure x, Liftp p x holds exactly when there exists a representation ⟨a,f⟩ of x such that x = abs ⟨a,f⟩ and p holds for all coordinates of f.
Русский
Для свойства p на α и структуры F утверждение Liftp p x эквивалентно существованию представления ⟨a,f⟩, такого что x = abs ⟨a,f⟩ и p выполняется для всех координат f.
LaTeX
$$$\\\\text{Liftp } p x \\\\iff \\\\exists a,f, x = abs ⟨a,f⟩ \\\\wedge \\\\forall i, p (f i).$$$
Lean4
theorem liftp_iff {α : Type u} (p : α → Prop) (x : F α) : Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ i, p (f i) :=
by
constructor
· rintro ⟨y, hy⟩
rcases h : repr y with ⟨a, f⟩
use a, fun i => (f i).val
constructor
· rw [← hy, ← abs_repr y, h, ← abs_map]
rfl
intro i
apply (f i).property
rintro ⟨a, f, h₀, h₁⟩
use abs ⟨a, fun i => ⟨f i, h₁ i⟩⟩
rw [← abs_map, h₀]; rfl
