supp_eq_of_isUniform — Mathlib

English

If q is uniform, then for any representation ⟨a,f⟩ and index i, supp(abs ⟨a,f⟩) i equals f i '' univ.

Русский

Если q однороден, то для любого представления ⟨a,f⟩ и индекса i опора(abs ⟨a,f⟩) i равна f i '' univ.

LaTeX

$$$$ \\forall i,\\ \\mathrm{supp}(\\mathrm{abs}\\langle a,f\\rangle)\\,i = f\\,i'' univ. $$$$

Lean4

theorem supp_eq_of_isUniform (h : q.IsUniform) {α : TypeVec n} (a : q.P.A) (f : q.P.B a ⟹ α) :
    ∀ i, supp (abs ⟨a, f⟩) i = f i '' univ := by
  intro; ext u; rw [mem_supp]; constructor
  · intro h'
    apply h' _ _ rfl
  intro h' a' f' e
  rw [← h _ _ _ _ e.symm]; apply h'

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