supp_eq_of_isUniform — Mathlib

English

If the IsUniform property h holds, then for any a and f, the support of abs ⟨a, f⟩ is exactly f'' univ.

Русский

Если выполняется свойство IsUniform, то для любого a и f поддержка abs ⟨a, f⟩ равна f'' univ.

LaTeX

$$$$\forall {F : Type u \to Type u} [q : QPF F] (h : q.IsUniform) {\alpha : Type u} (a : (q.P F).A) (f : (q.P F).B a \to α),\ supp (abs ⟨a, f⟩) = f '' univ.$$$$

Lean4

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

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