suppPreservation_iff_uniform — Mathlib

English

SuppPreservation is equivalent to IsUniform.

Русский

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

LaTeX

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

Lean4

theorem suppPreservation_iff_uniform : q.SuppPreservation ↔ q.IsUniform :=
  by
  constructor
  · intro h α a a' f f' h'
    rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]
  · rintro h α ⟨a, f⟩
    rwa [supp_eq_of_isUniform, PFunctor.supp_eq]

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