English
SuppPreservation is equivalent to LiftPPreservation.
Русский
Сохранение опоры эквивалентно сохранению LiftP.
LaTeX
$$$$ q.SuppPreservation \\iff q.LiftPPreservation $$$$
Lean4
theorem suppPreservation_iff_liftpPreservation : q.SuppPreservation ↔ q.LiftPPreservation :=
by
constructor <;> intro h
· rintro α p ⟨a, f⟩
have h' := h
rw [suppPreservation_iff_isUniform] at h'
dsimp only [SuppPreservation, supp] at h
simp only [liftP_iff_of_isUniform, supp_eq_of_isUniform, MvPFunctor.liftP_iff', h', image_univ, mem_range,
exists_imp]
constructor <;> intros <;> subst_vars <;> solve_by_elim
· rintro α ⟨a, f⟩
simp only [LiftPPreservation] at h
ext
simp only [supp, h, mem_setOf_eq]