suppPreservation_iff_liftpPreservation

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]

Похожие утверждения