suppPreservation_iff_liftpPreservation

English

SuppPreservation is equivalent to LiftpPreservation.

Русский

SuppPreservation эквивалентно LiftpPreservation.

LaTeX

$$$$\forall {F : Type u \to Type u} [q : QPF F],\ SuppPreservation \leftrightarrow LiftpPreservation.$$$$

Lean4

theorem suppPreservation_iff_liftpPreservation : q.SuppPreservation ↔ q.LiftpPreservation :=
  by
  constructor <;> intro h
  · rintro α p ⟨a, f⟩
    have h' := h
    rw [suppPreservation_iff_uniform] at h'
    dsimp only [SuppPreservation, supp] at h
    rw [liftp_iff_of_isUniform h', supp_eq_of_isUniform h', PFunctor.liftp_iff']
    simp only [image_univ, mem_range, exists_imp]
    constructor <;> intros <;> subst_vars <;> solve_by_elim
  · rintro α ⟨a, f⟩
    simp only [LiftpPreservation] at h
    simp only [supp, h]

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