suppPreservation_iff_isUniform — Mathlib

English

SuppPreservation holds if and only if IsUniform holds.

Русский

Сохранение опоры верно тогда и только тогда, когда выполняется однородность.

LaTeX

$$$$ q.SuppPreservation \\iff q.IsUniform $$$$

Lean4

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

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